MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbvarg Structured version   Visualization version   GIF version

Theorem csbvarg 4211
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.
StepHypRef Expression
1 elex 3417 . 2 (𝐴𝑉𝐴 ∈ V)
2 vex 3405 . . . . . 6 𝑦 ∈ V
3 df-csb 3740 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
4 sbcel2gv 3704 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
54abbi1dv 2938 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
63, 5syl5eq 2863 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
72, 6ax-mp 5 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
87csbeq2i 4201 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
9 csbco 3749 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
10 df-csb 3740 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
118, 9, 103eqtr3i 2847 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
12 sbcel2gv 3704 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1312abbi1dv 2938 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1411, 13syl5eq 2863 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
151, 14syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2157  {cab 2803  Vcvv 3402  [wsbc 3644  csb 3739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-v 3404  df-sbc 3645  df-csb 3740
This theorem is referenced by:  csbvargi  4212  sbccsb2  4214  csbfv  6463  ixpsnval  8158  csbwrdg  13565  swrdspsleq  13693  prmgaplem7  15998  telgsums  18612  ixpsnbasval  19438  scmatscm  20551  pm2mpf1lem  20833  pm2mpcoe1  20839  idpm2idmp  20840  pm2mpmhmlem2  20858  monmat2matmon  20863  pm2mp  20864  fvmptnn04if  20888  chfacfscmulfsupp  20898  cayhamlem4  20927  divcncf  23451  esum2dlem  30502  relowlpssretop  33547  rdgeqoa  33553  renegclALT  34761  cdlemk40  36716  cotrclrcl  38552  frege124d  38571  frege70  38745  frege72  38747  frege77  38752  frege91  38766  frege92  38767  frege116  38791  frege118  38793  frege120  38795  rusbcALT  39157  onfrALTlem5  39273  onfrALTlem4  39274  onfrALTlem5VD  39633  onfrALTlem4VD  39634  iccelpart  41962  ply1mulgsumlem4  42763
  Copyright terms: Public domain W3C validator