Theorem csbvarg 4387

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 3462	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		df-csb 3851	. . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥}
3		sbcel2gv 3808	. . . . . . . 8 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
4	3	eqabcdv 2871	. . . . . . 7 ⊢ (𝑦 ∈ V → {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} = 𝑦)
5	2, 4	eqtrid 2784	. . . . . 6 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑥 = 𝑦)
6	5	elv 3446	. . . . 5 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦
7	6	csbeq2i 3858	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑦⦌𝑦
8		csbcow 3865	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑥⦌𝑥
9		df-csb 3851	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌𝑦 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦}
10	7, 8, 9	3eqtr3i 2768	. . 3 ⊢ ⦋𝐴 / 𝑥⦌𝑥 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦}
11		sbcel2gv 3808	. . . 4 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴))
12	11	eqabcdv 2871	. . 3 ⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} = 𝐴)
13	10, 12	eqtrid 2784	. 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)
14	1, 13	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {cab 2715  Vcvv 3441  [wsbc 3741  ⦋csb 3850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-sbc 3742  df-csb 3851

This theorem is referenced by:  csbvargi  4388  sbccsb2  4390  2nreu  4397  csbfv  6882  ixpsnval  8842  csbwrdg  14471  swrdspsleq  14593  prmgaplem7  16989  telgsums  19926  ixpsnbasval  21164  scmatscm  22461  pm2mpf1lem  22742  pm2mpcoe1  22748  idpm2idmp  22749  pm2mpmhmlem2  22767  monmat2matmon  22772  pm2mp  22773  fvmptnn04if  22797  chfacfscmulfsupp  22807  cayhamlem4  22836  divcncf  25408  opsbc2ie  32532  esum2dlem  34230  relowlpssretop  37540  rdgeqoa  37546  renegclALT  39260  cdlemk40  41214  tfsconcatfv  43619  iscard4  43810  minregex  43811  cotrclrcl  44019  frege124d  44038  frege70  44210  frege72  44212  frege77  44217  frege91  44231  frege92  44232  frege116  44256  frege118  44258  frege120  44260  rusbcALT  44715  onfrALTlem5  44819  onfrALTlem4  44820  onfrALTlem5VD  45161  iccelpart  47715  ply1mulgsumlem4  48671