Theorem bj-csbsnlem

Description: Lemma for bj-csbsn (in this lemma, x cannot occur in A ). (Contributed by BJ, 6-Oct-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-csbsnlem	$$⊢⦋A/x⦌\left\{x\right\}=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		abid	$$⊢y\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in \left\{x\right\}\right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in \left\{x\right\}$$
2		df-sbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in \left\{x\right\}\leftrightarrow A\in \left\{x|y\in \left\{x\right\}\right\}$$
3		clelab	$$⊢A\in \left\{x|y\in \left\{x\right\}\right\}\leftrightarrow \exists x\left(x=A\wedge y\in \left\{x\right\}\right)$$
4		velsn	$$⊢y\in \left\{x\right\}\leftrightarrow y=x$$
5	4	anbi2i	$$⊢\left(x=A\wedge y\in \left\{x\right\}\right)\leftrightarrow \left(x=A\wedge y=x\right)$$
6	5	exbii	$$⊢\exists x\left(x=A\wedge y\in \left\{x\right\}\right)\leftrightarrow \exists x\left(x=A\wedge y=x\right)$$
7		eqeq2	$$⊢x=A\to \left(y=x\leftrightarrow y=A\right)$$
8	7	pm5.32i	$$⊢\left(x=A\wedge y=x\right)\leftrightarrow \left(x=A\wedge y=A\right)$$
9	8	exbii	$$⊢\exists x\left(x=A\wedge y=x\right)\leftrightarrow \exists x\left(x=A\wedge y=A\right)$$
10		19.41v	$$⊢\exists x\left(x=A\wedge y=A\right)\leftrightarrow \left(\exists xx=A\wedge y=A\right)$$
11		simpr	$$⊢\left(\exists xx=A\wedge y=A\right)\to y=A$$
12		eqvisset	$$⊢y=A\to A\in \mathrm{V}$$
13		elisset	$$⊢A\in \mathrm{V}\to \exists xx=A$$
14	12 13	syl	$$⊢y=A\to \exists xx=A$$
15	14	ancri	$$⊢y=A\to \left(\exists xx=A\wedge y=A\right)$$
16	11 15	impbii	$$⊢\left(\exists xx=A\wedge y=A\right)\leftrightarrow y=A$$
17	9 10 16	3bitri	$$⊢\exists x\left(x=A\wedge y=x\right)\leftrightarrow y=A$$
18	3 6 17	3bitri	$$⊢A\in \left\{x|y\in \left\{x\right\}\right\}\leftrightarrow y=A$$
19	1 2 18	3bitri	$$⊢y\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in \left\{x\right\}\right\}\leftrightarrow y=A$$
20		df-csb	$$⊢⦋A/x⦌\left\{x\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in \left\{x\right\}\right\}$$
21	20	eleq2i	$$⊢y\in ⦋A/x⦌\left\{x\right\}\leftrightarrow y\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in \left\{x\right\}\right\}$$
22		velsn	$$⊢y\in \left\{A\right\}\leftrightarrow y=A$$
23	19 21 22	3bitr4i	$$⊢y\in ⦋A/x⦌\left\{x\right\}\leftrightarrow y\in \left\{A\right\}$$
24	23	eqriv	$$⊢⦋A/x⦌\left\{x\right\}=\left\{A\right\}$$