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