Theorem csbvarg

Description: The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005)

	Ref	Expression
Assertion	csbvarg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑥 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		df-csb	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝑥 = { 𝑧 ∣ [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝑥 }
3		sbcel2gv	⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) )
4	3	abbi1dv	⊢ ( 𝑦 ∈ V → { 𝑧 ∣ [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝑥 } = 𝑦 )
5	2 4	eqtrid	⊢ ( 𝑦 ∈ V → ⦋ 𝑦 / 𝑥 ⦌ 𝑥 = 𝑦 )
6	5	elv	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝑥 = 𝑦
7	6	csbeq2i	⊢ ⦋ 𝐴 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝑥 = ⦋ 𝐴 / 𝑦 ⦌ 𝑦
8		csbcow	⊢ ⦋ 𝐴 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝑥 = ⦋ 𝐴 / 𝑥 ⦌ 𝑥
9		df-csb	⊢ ⦋ 𝐴 / 𝑦 ⦌ 𝑦 = { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝑦 }
10	7 8 9	3eqtr3i	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝑥 = { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝑦 }
11		sbcel2gv	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴 ) )
12	11	abbi1dv	⊢ ( 𝐴 ∈ V → { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝑦 } = 𝐴 )
13	10 12	eqtrid	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝑥 = 𝐴 )
14	1 13	syl	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑥 = 𝐴 )