Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The difference, union, and intersection of two classes
The union of two classes
ssun2
Next ⟩
ssun3
Metamath Proof Explorer
Ascii
Unicode
Theorem
ssun2
Description:
Subclass relationship for union of classes.
(Contributed by
NM
, 30-Aug-1993)
Ref
Expression
Assertion
ssun2
⊢
A
⊆
B
∪
A
Proof
Step
Hyp
Ref
Expression
1
ssun1
⊢
A
⊆
A
∪
B
2
uncom
⊢
A
∪
B
=
B
∪
A
3
1
2
sseqtri
⊢
A
⊆
B
∪
A