Theorem frege54cor1c

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

	Ref	Expression
Hypothesis	frege54c.1	⊢ 𝐴 ∈ 𝐶
Assertion	frege54cor1c	⊢ [ 𝐴 / 𝑥 ] 𝑥 = 𝐴

Proof

Step	Hyp	Ref	Expression
1		frege54c.1	⊢ 𝐴 ∈ 𝐶
2	1	elexi	⊢ 𝐴 ∈ V
3	2	snid	⊢ 𝐴 ∈ { 𝐴 }
4		df-sn	⊢ { 𝐴 } = { 𝑥 ∣ 𝑥 = 𝐴 }
5	3 4	eleqtri	⊢ 𝐴 ∈ { 𝑥 ∣ 𝑥 = 𝐴 }
6		df-sbc	⊢ ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐴 ↔ 𝐴 ∈ { 𝑥 ∣ 𝑥 = 𝐴 } )
7	5 6	mpbir	⊢ [ 𝐴 / 𝑥 ] 𝑥 = 𝐴