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