This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqabcdv ⊢ ( 𝑦 ∈ 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 eqabcdv ⊢ ( 𝐴 ∈ V → { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝑦 } = 𝐴 )
13 10 12 eqtrid ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝑥 = 𝐴 )
14 1 13 syl ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑥 = 𝐴 )