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 | ⊢ 𝐴 = 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | ⊢ 𝐴 | |
| 1 | 0 0 | wceq | ⊢ 𝐴 = 𝐴 |