Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Introduce the Axiom of Union
unexd
Next ⟩
sqxpexg
Metamath Proof Explorer
Ascii
Unicode
Theorem
unexd
Description:
The union of two sets is a set.
(Contributed by
SN
, 16-Jul-2024)
Ref
Expression
Hypotheses
unexd.1
⊢
φ
→
A
∈
V
unexd.2
⊢
φ
→
B
∈
W
Assertion
unexd
⊢
φ
→
A
∪
B
∈
V
Proof
Step
Hyp
Ref
Expression
1
unexd.1
⊢
φ
→
A
∈
V
2
unexd.2
⊢
φ
→
B
∈
W
3
unexg
⊢
A
∈
V
∧
B
∈
W
→
A
∪
B
∈
V
4
1
2
3
syl2anc
⊢
φ
→
A
∪
B
∈
V