Theorem csbvarg 4375

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 3451	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		df-csb 3839	. . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥}
3		sbcel2gv 3796	. . . . . . . 8 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
4	3	eqabcdv 2871	. . . . . . 7 ⊢ (𝑦 ∈ V → {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} = 𝑦)
5	2, 4	eqtrid 2784	. . . . . 6 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑥 = 𝑦)
6	5	elv 3435	. . . . 5 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦
7	6	csbeq2i 3846	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑦⦌𝑦
8		csbcow 3853	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑥⦌𝑥
9		df-csb 3839	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌𝑦 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦}
10	7, 8, 9	3eqtr3i 2768	. . 3 ⊢ ⦋𝐴 / 𝑥⦌𝑥 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦}
11		sbcel2gv 3796	. . . 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 3430  [wsbc 3729  ⦋csb 3838

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 3432  df-sbc 3730  df-csb 3839

This theorem is referenced by:  csbvargi  4376  sbccsb2  4378  2nreu  4385  csbfv  6879  ixpsnval  8839  csbwrdg  14495  swrdspsleq  14617  prmgaplem7  17017  telgsums  19957  ixpsnbasval  21193  scmatscm  22487  pm2mpf1lem  22768  pm2mpcoe1  22774  idpm2idmp  22775  pm2mpmhmlem2  22793  monmat2matmon  22798  pm2mp  22799  fvmptnn04if  22823  chfacfscmulfsupp  22833  cayhamlem4  22862  divcncf  25423  opsbc2ie  32565  esum2dlem  34257  relowlpssretop  37691  rdgeqoa  37697  renegclALT  39420  cdlemk40  41374  tfsconcatfv  43784  iscard4  43975  minregex  43976  cotrclrcl  44184  frege124d  44203  frege70  44375  frege72  44377  frege77  44382  frege91  44396  frege92  44397  frege116  44421  frege118  44423  frege120  44425  rusbcALT  44880  onfrALTlem5  44984  onfrALTlem4  44985  onfrALTlem5VD  45326  iccelpart  47890  ply1mulgsumlem4  48862