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

Theorem csbvarg 4292
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 3450 . 2 (𝐴𝑉𝐴 ∈ V)
2 df-csb 3807 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
3 sbcel2gv 3764 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
43abbi1dv 2919 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
52, 4syl5eq 2841 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
65elv 3437 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
76csbeq2i 3814 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
8 csbco 3820 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
9 df-csb 3807 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
107, 8, 93eqtr3i 2825 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
11 sbcel2gv 3764 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1211abbi1dv 2919 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1310, 12syl5eq 2841 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
141, 13syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1520  wcel 2079  {cab 2773  Vcvv 3432  [wsbc 3701  csb 3806
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-v 3434  df-sbc 3702  df-csb 3807
This theorem is referenced by:  csbvargi  4293  sbccsb2  4295  2nreu  4301  csbfv  6575  ixpsnval  8303  csbwrdg  13729  swrdspsleq  13851  prmgaplem7  16210  telgsums  18818  ixpsnbasval  19659  scmatscm  20794  pm2mpf1lem  21074  pm2mpcoe1  21080  idpm2idmp  21081  pm2mpmhmlem2  21099  monmat2matmon  21104  pm2mp  21105  fvmptnn04if  21129  chfacfscmulfsupp  21139  cayhamlem4  21168  divcncf  23719  opsbc2ie  29918  esum2dlem  30924  relowlpssretop  34122  rdgeqoa  34128  renegclALT  35580  cdlemk40  37534  iscard4  39336  cotrclrcl  39523  frege124d  39542  frege70  39715  frege72  39717  frege77  39722  frege91  39736  frege92  39737  frege116  39761  frege118  39763  frege120  39765  rusbcALT  40261  onfrALTlem5  40367  onfrALTlem4  40368  onfrALTlem5VD  40710  iccelpart  43029  ply1mulgsumlem4  43877
  Copyright terms: Public domain W3C validator