Theorem csbvarg 4434

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 3501	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		df-csb 3900	. . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥}
3		sbcel2gv 3857	. . . . . . . 8 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
4	3	eqabcdv 2876	. . . . . . 7 ⊢ (𝑦 ∈ V → {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} = 𝑦)
5	2, 4	eqtrid 2789	. . . . . 6 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑥 = 𝑦)
6	5	elv 3485	. . . . 5 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦
7	6	csbeq2i 3907	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑦⦌𝑦
8		csbcow 3914	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑥⦌𝑥
9		df-csb 3900	. . . 4 ⊢ ⦋𝐴 / 𝑦⦌𝑦 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦}
10	7, 8, 9	3eqtr3i 2773	. . 3 ⊢ ⦋𝐴 / 𝑥⦌𝑥 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦}
11		sbcel2gv 3857	. . . 4 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴))
12	11	eqabcdv 2876	. . 3 ⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} = 𝐴)
13	10, 12	eqtrid 2789	. 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)
14	1, 13	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {cab 2714  Vcvv 3480  [wsbc 3788  ⦋csb 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-sbc 3789  df-csb 3900

This theorem is referenced by:  csbvargi  4435  sbccsb2  4437  2nreu  4444  csbfv  6956  ixpsnval  8940  csbwrdg  14582  swrdspsleq  14703  prmgaplem7  17095  telgsums  20011  ixpsnbasval  21215  scmatscm  22519  pm2mpf1lem  22800  pm2mpcoe1  22806  idpm2idmp  22807  pm2mpmhmlem2  22825  monmat2matmon  22830  pm2mp  22831  fvmptnn04if  22855  chfacfscmulfsupp  22865  cayhamlem4  22894  divcncf  25482  opsbc2ie  32495  esum2dlem  34093  relowlpssretop  37365  rdgeqoa  37371  renegclALT  38964  cdlemk40  40919  tfsconcatfv  43354  iscard4  43546  minregex  43547  cotrclrcl  43755  frege124d  43774  frege70  43946  frege72  43948  frege77  43953  frege91  43967  frege92  43968  frege116  43992  frege118  43994  frege120  43996  rusbcALT  44458  onfrALTlem5  44562  onfrALTlem4  44563  onfrALTlem5VD  44905  iccelpart  47420  ply1mulgsumlem4  48306