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

Theorem csbvarg 4389
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 3461 . 2 (𝐴𝑉𝐴 ∈ V)
2 df-csb 3854 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
3 sbcel2gv 3809 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
43abbi1dv 2877 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
52, 4eqtrid 2788 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
65elv 3449 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
76csbeq2i 3861 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
8 csbcow 3868 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
9 df-csb 3854 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
107, 8, 93eqtr3i 2772 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
11 sbcel2gv 3809 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1211abbi1dv 2877 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1310, 12eqtrid 2788 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
141, 13syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  {cab 2713  Vcvv 3443  [wsbc 3737  csb 3853
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3445  df-sbc 3738  df-csb 3854
This theorem is referenced by:  csbvargi  4390  sbccsb2  4392  2nreu  4399  csbfv  6889  ixpsnval  8834  csbwrdg  14424  swrdspsleq  14545  prmgaplem7  16921  telgsums  19761  ixpsnbasval  20664  scmatscm  21846  pm2mpf1lem  22127  pm2mpcoe1  22133  idpm2idmp  22134  pm2mpmhmlem2  22152  monmat2matmon  22157  pm2mp  22158  fvmptnn04if  22182  chfacfscmulfsupp  22192  cayhamlem4  22221  divcncf  24795  opsbc2ie  31290  esum2dlem  32560  relowlpssretop  35802  rdgeqoa  35808  renegclALT  37392  cdlemk40  39347  iscard4  41747  minregex  41748  cotrclrcl  41956  frege124d  41975  frege70  42147  frege72  42149  frege77  42154  frege91  42168  frege92  42169  frege116  42193  frege118  42195  frege120  42197  rusbcALT  42661  onfrALTlem5  42766  onfrALTlem4  42767  onfrALTlem5VD  43109  iccelpart  45557  ply1mulgsumlem4  46402
  Copyright terms: Public domain W3C validator