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

Theorem csbvarg 4435
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 3492 . 2 (𝐴𝑉𝐴 ∈ V)
2 df-csb 3895 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
3 sbcel2gv 3850 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
43eqabcdv 2864 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
52, 4eqtrid 2780 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
65elv 3479 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
76csbeq2i 3902 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
8 csbcow 3909 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
9 df-csb 3895 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
107, 8, 93eqtr3i 2764 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
11 sbcel2gv 3850 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1211eqabcdv 2864 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1310, 12eqtrid 2780 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
141, 13syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wcel 2098  {cab 2705  Vcvv 3473  [wsbc 3778  csb 3894
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-12 2166  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-sbc 3779  df-csb 3895
This theorem is referenced by:  csbvargi  4436  sbccsb2  4438  2nreu  4445  csbfv  6952  ixpsnval  8925  csbwrdg  14534  swrdspsleq  14655  prmgaplem7  17033  telgsums  19955  ixpsnbasval  21108  scmatscm  22435  pm2mpf1lem  22716  pm2mpcoe1  22722  idpm2idmp  22723  pm2mpmhmlem2  22741  monmat2matmon  22746  pm2mp  22747  fvmptnn04if  22771  chfacfscmulfsupp  22781  cayhamlem4  22810  divcncf  25396  opsbc2ie  32295  esum2dlem  33744  relowlpssretop  36876  rdgeqoa  36882  renegclALT  38467  cdlemk40  40422  tfsconcatfv  42801  iscard4  42994  minregex  42995  cotrclrcl  43203  frege124d  43222  frege70  43394  frege72  43396  frege77  43401  frege91  43415  frege92  43416  frege116  43440  frege118  43442  frege120  43444  rusbcALT  43907  onfrALTlem5  44012  onfrALTlem4  44013  onfrALTlem5VD  44355  iccelpart  46802  ply1mulgsumlem4  47535
  Copyright terms: Public domain W3C validator