Theorem una

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: diff-int-01, diff-subset, diff-supset-empty, diff-union, diff-union-01, diff-union-02, diff-union-03, intu-empty, k-union-base, k-union-rec1, k-union-rec2, rem-union-ins, size-union, sub-union, sub-union-01, sub-union-02, sub-union-03, sub-union-04, sub-union-05, subset-is-union, unadd, unadd-01, unall, unc, undel, undel-01, undel-02, undel-03, undel-04, undel-06, une, une-01, uneq, unidem, unin, unin-01, unindel, uninsert, uninsubdel, union-del, union-diff, union-diff-union-same, union-difference, union-inter-inter-union, union-one, union-rem-add, union-rem-unchdg, union-rewone, union-size, union-size-01, union-size-02, union-size-03, union-size-insert, union-size-le, union-sizeeq, union-sizele, union-sub, union-sub-01, union-subset, union-subset-01, union-subset-02, union-subset-03, union-subset-04, union-subset-05, union-subseteq-union-same, unsub, unsub-union-01, unsubdel, unsubdel-01, unsubins, unsubins-01, unsubsub,
• Used by units in proved state: oset,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 0
• Proof steps: 1
• Used lemmas: unrax,
• Used spec theorems:
  • Used simplifier rules:
    • set-basic/Extension