Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Classes
Class equality
eqidd
Next ⟩
eqeq1d
Metamath Proof Explorer
Ascii
Unicode
Theorem
eqidd
Description:
Class identity law with antecedent.
(Contributed by
NM
, 21-Aug-2008)
Ref
Expression
Assertion
eqidd
$${\u22a2}{\phi}\to {A}={A}$$
Proof
Step
Hyp
Ref
Expression
1
eqid
$${\u22a2}{A}={A}$$
2
1
a1i
$${\u22a2}{\phi}\to {A}={A}$$