Metamath Proof Explorer


Axiom ax-frege54c

Description: Reflexive equality of sets (as classes). Part of Axiom 54 of Frege1879 p. 50. Identical to eqid . (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)

Ref Expression
Assertion ax-frege54c 𝐴 = 𝐴

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 0 0 wceq 𝐴 = 𝐴