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

Theorem csbvarg 4339
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 3459 . 2 (𝐴𝑉𝐴 ∈ V)
2 df-csb 3829 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
3 sbcel2gv 3787 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
43abbi1dv 2928 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
52, 4syl5eq 2845 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
65elv 3446 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
76csbeq2i 3836 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
8 csbcow 3843 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
9 df-csb 3829 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
107, 8, 93eqtr3i 2829 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
11 sbcel2gv 3787 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1211abbi1dv 2928 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1310, 12syl5eq 2845 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
141, 13syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2111  {cab 2776  Vcvv 3441  [wsbc 3720  csb 3828
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-sbc 3721  df-csb 3829
This theorem is referenced by:  csbvargi  4340  sbccsb2  4342  2nreu  4349  csbfv  6690  ixpsnval  8447  csbwrdg  13887  swrdspsleq  14018  prmgaplem7  16383  telgsums  19106  ixpsnbasval  19975  scmatscm  21118  pm2mpf1lem  21399  pm2mpcoe1  21405  idpm2idmp  21406  pm2mpmhmlem2  21424  monmat2matmon  21429  pm2mp  21430  fvmptnn04if  21454  chfacfscmulfsupp  21464  cayhamlem4  21493  divcncf  24051  opsbc2ie  30246  esum2dlem  31461  relowlpssretop  34781  rdgeqoa  34787  renegclALT  36259  cdlemk40  38213  iscard4  40239  cotrclrcl  40441  frege124d  40460  frege70  40632  frege72  40634  frege77  40639  frege91  40653  frege92  40654  frege116  40678  frege118  40680  frege120  40682  rusbcALT  41141  onfrALTlem5  41246  onfrALTlem4  41247  onfrALTlem5VD  41589  iccelpart  43948  ply1mulgsumlem4  44795
  Copyright terms: Public domain W3C validator