Theorem frege54cor1c

Description: Reflexive equality. (Contributed by RP, 24-Dec-2019) (Revised by RP, 25-Apr-2020)

	Ref	Expression
Hypothesis	frege54c.1	|- A e. C
Assertion	frege54cor1c	|- [. A / x ]. x = A

Proof

Step	Hyp	Ref	Expression
1		frege54c.1	|- A e. C
2	1	elexi	|- A e. _V
3	2	snid	|- A e. { A }
4		df-sn	|- { A } = { x | x = A }
5	3 4	eleqtri	|- A e. { x | x = A }
6		df-sbc	|- ( [. A / x ]. x = A <-> A e. { x | x = A } )
7	5 6	mpbir	|- [. A / x ]. x = A