Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Unordered and ordered pairs
elunsn
Next ⟩
elpwunsn
Metamath Proof Explorer
Ascii
Unicode
Theorem
elunsn
Description:
Elementhood in a union with a singleton.
(Contributed by
Thierry Arnoux
, 14-Dec-2023)
Ref
Expression
Assertion
elunsn
⊢
A
∈
V
→
A
∈
B
∪
C
↔
A
∈
B
∨
A
=
C
Proof
Step
Hyp
Ref
Expression
1
elun
⊢
A
∈
B
∪
C
↔
A
∈
B
∨
A
∈
C
2
elsng
⊢
A
∈
V
→
A
∈
C
↔
A
=
C
3
2
orbi2d
⊢
A
∈
V
→
A
∈
B
∨
A
∈
C
↔
A
∈
B
∨
A
=
C
4
1
3
bitrid
⊢
A
∈
V
→
A
∈
B
∪
C
↔
A
∈
B
∨
A
=
C