Theorem csbvarg 4391

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

Assertion

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

Proof of Theorem csbvarg

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3471	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		df-csb 3847	. . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥}
3		sbcel2gv 3804	. . . . . . . 8 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
4	3	eqabcdv 2894	. . . . . . 7 ⊢ (𝑦 ∈ V → {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} = 𝑦)
5	2, 4	eqtrid 2807	. . . . . 6 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑥 = 𝑦)
6	5	elv 3455	. . . . 5 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦
7	6	csbeq2i 3854	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑦⦌𝑦
8		csbcow 3861	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑥⦌𝑥
9		df-csb 3847	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌𝑦 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦}
10	7, 8, 9	3eqtr3i 2791	. . 3 ⊢ ⦋𝐴 / 𝑥⦌𝑥 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦}
11		sbcel2gv 3804	. . . 4 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴))
12	11	eqabcdv 2894	. . 3 ⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} = 𝐴)
13	10, 12	eqtrid 2807	. 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)
14	1, 13	syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {cab 2738  Vcvv 3450  [wsbc 3738  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sbc 3739  df-csb 3847

This theorem is used by:  csbvargi  4392  sbccsb2  4394  2nreu  4401  csbfv  6932  ixpsnval  8929  csbwrdg  14690  swrdspsleq  14816  prmgaplem7  17236  telgsums  20208  ixpsnbasval  21484  scmatscm  22829  pm2mpf1lem  23113  pm2mpcoe1  23119  idpm2idmp  23120  pm2mpmhmlem2  23138  monmat2matmon  23143  pm2mp  23144  fvmptnn04if  23168  chfacfscmulfsupp  23178  cayhamlem4  23207  divcncf  25769  opsbc2ie  33115  esum2dlem  34767  relowlpssretop  38363  rdgeqoa  38369  renegclALT  40096  cdlemk40  42050  tfsconcatfv  44419  iscard4  44610  minregex  44611  cotrclrcl  44818  frege124d  44837  frege70  45009  frege72  45011  frege77  45016  frege91  45030  frege92  45031  frege116  45055  frege118  45057  frege120  45059  rusbcALT  45498  onfrALTlem5  45601  onfrALTlem4  45602  onfrALTlem5VD  45943  iccelpart  48591  ply1mulgsumlem4  49577