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 ⊢ A ∈ V → ⦋ A / x⦌ x = A

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ V → A ∈ V
2 df-csb ⊢ ⦋ y / x⦌ x = z | [˙y / x]˙ z ∈ x
3 sbcel2gv ⊢ y ∈ V → [˙y / x]˙ z ∈ x ↔ z ∈ y
4 3 eqabcdv ⊢ y ∈ V → z | [˙y / x]˙ z ∈ x = y
5 2 4 eqtrid ⊢ y ∈ V → ⦋ y / x⦌ x = y
6 5 elv ⊢ ⦋ y / x⦌ x = y
7 6 csbeq2i ⊢ ⦋ A / y⦌ ⦋ y / x⦌ x = ⦋ A / y⦌ y
8 csbcow ⊢ ⦋ A / y⦌ ⦋ y / x⦌ x = ⦋ A / x⦌ x
9 df-csb ⊢ ⦋ A / y⦌ y = z | [˙A / y]˙ z ∈ y
10 7 8 9 3eqtr3i ⊢ ⦋ A / x⦌ x = z | [˙A / y]˙ z ∈ y
11 sbcel2gv ⊢ A ∈ V → [˙A / y]˙ z ∈ y ↔ z ∈ A
12 11 eqabcdv ⊢ A ∈ V → z | [˙A / y]˙ z ∈ y = A
13 10 12 eqtrid ⊢ A ∈ V → ⦋ A / x⦌ x = A
14 1 13 syl ⊢ A ∈ V → ⦋ A / x⦌ x = A