Theorem csbvarg 4430

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  {cab 2707  Vcvv 3472  [wsbc 3776  ⦋csb 3892

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-sbc 3777  df-csb 3893

This theorem is referenced by:  csbvargi  4431  sbccsb2  4433  2nreu  4440  csbfv  6940  ixpsnval  8896  csbwrdg  14498  swrdspsleq  14619  prmgaplem7  16994  telgsums  19902  ixpsnbasval  20977  scmatscm  22235  pm2mpf1lem  22516  pm2mpcoe1  22522  idpm2idmp  22523  pm2mpmhmlem2  22541  monmat2matmon  22546  pm2mp  22547  fvmptnn04if  22571  chfacfscmulfsupp  22581  cayhamlem4  22610  divcncf  25196  opsbc2ie  31983  esum2dlem  33388  relowlpssretop  36548  rdgeqoa  36554  renegclALT  38136  cdlemk40  40091  tfsconcatfv  42393  iscard4  42586  minregex  42587  cotrclrcl  42795  frege124d  42814  frege70  42986  frege72  42988  frege77  42993  frege91  43007  frege92  43008  frege116  43032  frege118  43034  frege120  43036  rusbcALT  43500  onfrALTlem5  43605  onfrALTlem4  43606  onfrALTlem5VD  43948  iccelpart  46399  ply1mulgsumlem4  47157