Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Unordered and ordered pairs
tpeq1d
Next ⟩
tpeq2d
Metamath Proof Explorer
Ascii
Unicode
Theorem
tpeq1d
Description:
Equality theorem for unordered triples.
(Contributed by
NM
, 22-Jun-2014)
Ref
Expression
Hypothesis
tpeq1d.1
⊢
φ
→
A
=
B
Assertion
tpeq1d
⊢
φ
→
A
C
D
=
B
C
D
Proof
Step
Hyp
Ref
Expression
1
tpeq1d.1
⊢
φ
→
A
=
B
2
tpeq1
⊢
A
=
B
→
A
C
D
=
B
C
D
3
1
2
syl
⊢
φ
→
A
C
D
=
B
C
D