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	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 } = { 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ { 𝑥 } } ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ { 𝑥 } )
2		df-sbc	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ { 𝑥 } ↔ 𝐴 ∈ { 𝑥 ∣ 𝑦 ∈ { 𝑥 } } )
3		clelab	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝑦 ∈ { 𝑥 } } ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑦 ∈ { 𝑥 } ) )
4		velsn	⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 )
5	4	anbi2i	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 ∈ { 𝑥 } ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑥 ) )
6	5	exbii	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑦 ∈ { 𝑥 } ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑥 ) )
7		eqeq2	⊢ ( 𝑥 = 𝐴 → ( 𝑦 = 𝑥 ↔ 𝑦 = 𝐴 ) )
8	7	pm5.32i	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
9	8	exbii	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
10		19.41v	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
11		simpr	⊢ ( ( ∃ 𝑥 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) → 𝑦 = 𝐴 )
12		eqvisset	⊢ ( 𝑦 = 𝐴 → 𝐴 ∈ V )
13		elisset	⊢ ( 𝐴 ∈ V → ∃ 𝑥 𝑥 = 𝐴 )
14	12 13	syl	⊢ ( 𝑦 = 𝐴 → ∃ 𝑥 𝑥 = 𝐴 )
15	14	ancri	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
16	11 15	impbii	⊢ ( ( ∃ 𝑥 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) ↔ 𝑦 = 𝐴 )
17	9 10 16	3bitri	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑥 ) ↔ 𝑦 = 𝐴 )
18	3 6 17	3bitri	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝑦 ∈ { 𝑥 } } ↔ 𝑦 = 𝐴 )
19	1 2 18	3bitri	⊢ ( 𝑦 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ { 𝑥 } } ↔ 𝑦 = 𝐴 )
20		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ { 𝑥 } }
21	20	eleq2i	⊢ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 } ↔ 𝑦 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ { 𝑥 } } )
22		velsn	⊢ ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 )
23	19 21 22	3bitr4i	⊢ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 } ↔ 𝑦 ∈ { 𝐴 } )
24	23	eqriv	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 } = { 𝐴 }