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

Theorem csbvarg 4439
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 3498 . 2 (𝐴𝑉𝐴 ∈ V)
2 df-csb 3908 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
3 sbcel2gv 3862 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
43eqabcdv 2873 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
52, 4eqtrid 2786 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
65elv 3482 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
76csbeq2i 3915 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
8 csbcow 3922 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
9 df-csb 3908 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
107, 8, 93eqtr3i 2770 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
11 sbcel2gv 3862 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1211eqabcdv 2873 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1310, 12eqtrid 2786 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
141, 13syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1536  wcel 2105  {cab 2711  Vcvv 3477  [wsbc 3790  csb 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-12 2174  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-sbc 3791  df-csb 3908
This theorem is referenced by:  csbvargi  4440  sbccsb2  4442  2nreu  4449  csbfv  6956  ixpsnval  8938  csbwrdg  14578  swrdspsleq  14699  prmgaplem7  17090  telgsums  20025  ixpsnbasval  21232  scmatscm  22534  pm2mpf1lem  22815  pm2mpcoe1  22821  idpm2idmp  22822  pm2mpmhmlem2  22840  monmat2matmon  22845  pm2mp  22846  fvmptnn04if  22870  chfacfscmulfsupp  22880  cayhamlem4  22909  divcncf  25495  opsbc2ie  32503  esum2dlem  34072  relowlpssretop  37346  rdgeqoa  37352  renegclALT  38944  cdlemk40  40899  tfsconcatfv  43330  iscard4  43522  minregex  43523  cotrclrcl  43731  frege124d  43750  frege70  43922  frege72  43924  frege77  43929  frege91  43943  frege92  43944  frege116  43968  frege118  43970  frege120  43972  rusbcALT  44434  onfrALTlem5  44539  onfrALTlem4  44540  onfrALTlem5VD  44882  iccelpart  47357  ply1mulgsumlem4  48234
  Copyright terms: Public domain W3C validator