Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Classes
Class equality
eqtr3
Next ⟩
eqtri
Metamath Proof Explorer
Ascii
Unicode
Theorem
eqtr3
Description:
A transitive law for class equality.
(Contributed by
NM
, 20-May-2005)
Ref
Expression
Assertion
eqtr3
⊢
A
=
C
∧
B
=
C
→
A
=
B
Proof
Step
Hyp
Ref
Expression
1
eqcom
⊢
B
=
C
↔
C
=
B
2
eqtr
⊢
A
=
C
∧
C
=
B
→
A
=
B
3
1
2
sylan2b
⊢
A
=
C
∧
B
=
C
→
A
=
B