Theorem frege54cor1c

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

	Ref	Expression
Hypothesis	frege54c.1	$$⊢A\in C$$
Assertion	frege54cor1c	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x=A$$

Proof

Step	Hyp	Ref	Expression
1		frege54c.1	$$⊢A\in C$$
2	1	elexi	$$⊢A\in \mathrm{V}$$
3	2	snid	$$⊢A\in \left\{A\right\}$$
4		df-sn	$$⊢\left\{A\right\}=\left\{x|x=A\right\}$$
5	3 4	eleqtri	$$⊢A\in \left\{x|x=A\right\}$$
6		df-sbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x=A\leftrightarrow A\in \left\{x|x=A\right\}$$
7	5 6	mpbir	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x=A$$