Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Unordered and ordered pairs
tpid2g
Next ⟩
tpid3g
Metamath Proof Explorer
Ascii
Unicode
Theorem
tpid2g
Description:
Closed theorem form of
tpid2
.
(Contributed by
Glauco Siliprandi
, 23-Oct-2021)
Ref
Expression
Assertion
tpid2g
⊢
A
∈
B
→
A
∈
C
A
D
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
A
=
A
2
1
3mix2i
⊢
A
=
C
∨
A
=
A
∨
A
=
D
3
eltpg
⊢
A
∈
B
→
A
∈
C
A
D
↔
A
=
C
∨
A
=
A
∨
A
=
D
4
2
3
mpbiri
⊢
A
∈
B
→
A
∈
C
A
D