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 ]_ { x } = { A }

Proof

Step	Hyp	Ref	Expression
1		abid	|- ( y e. { y | [. A / x ]. y e. { x } } <-> [. A / x ]. y e. { x } )
2		df-sbc	|- ( [. A / x ]. y e. { x } <-> A e. { x | y e. { x } } )
3		clelab	|- ( A e. { x | y e. { x } } <-> E. x ( x = A /\ y e. { x } ) )
4		velsn	|- ( y e. { x } <-> y = x )
5	4	anbi2i	|- ( ( x = A /\ y e. { x } ) <-> ( x = A /\ y = x ) )
6	5	exbii	|- ( E. x ( x = A /\ y e. { x } ) <-> E. x ( x = A /\ y = x ) )
7		eqeq2	|- ( x = A -> ( y = x <-> y = A ) )
8	7	pm5.32i	|- ( ( x = A /\ y = x ) <-> ( x = A /\ y = A ) )
9	8	exbii	|- ( E. x ( x = A /\ y = x ) <-> E. x ( x = A /\ y = A ) )
10		19.41v	|- ( E. x ( x = A /\ y = A ) <-> ( E. x x = A /\ y = A ) )
11		simpr	|- ( ( E. x x = A /\ y = A ) -> y = A )
12		eqvisset	|- ( y = A -> A e. _V )
13		elisset	|- ( A e. _V -> E. x x = A )
14	12 13	syl	|- ( y = A -> E. x x = A )
15	14	ancri	|- ( y = A -> ( E. x x = A /\ y = A ) )
16	11 15	impbii	|- ( ( E. x x = A /\ y = A ) <-> y = A )
17	9 10 16	3bitri	|- ( E. x ( x = A /\ y = x ) <-> y = A )
18	3 6 17	3bitri	|- ( A e. { x | y e. { x } } <-> y = A )
19	1 2 18	3bitri	|- ( y e. { y | [. A / x ]. y e. { x } } <-> y = A )
20		df-csb	|- [_ A / x ]_ { x } = { y | [. A / x ]. y e. { x } }
21	20	eleq2i	|- ( y e. [_ A / x ]_ { x } <-> y e. { y | [. A / x ]. y e. { x } } )
22		velsn	|- ( y e. { A } <-> y = A )
23	19 21 22	3bitr4i	|- ( y e. [_ A / x ]_ { x } <-> y e. { A } )
24	23	eqriv	|- [_ A / x ]_ { x } = { A }