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
elun2
Next ⟩
elunant
Metamath Proof Explorer
Ascii
Unicode
Theorem
elun2
Description:
Membership law for union of classes.
(Contributed by
NM
, 30-Aug-1993)
Ref
Expression
Assertion
elun2
⊢
A
∈
B
→
A
∈
C
∪
B
Proof
Step
Hyp
Ref
Expression
1
ssun2
⊢
B
⊆
C
∪
B
2
1
sseli
⊢
A
∈
B
→
A
∈
C
∪
B