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

Theorem csbvarg 4432
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 3493 . 2 (𝐴𝑉𝐴 ∈ V)
2 df-csb 3895 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
3 sbcel2gv 3850 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
43eqabcdv 2869 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
52, 4eqtrid 2785 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
65elv 3481 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
76csbeq2i 3902 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
8 csbcow 3909 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
9 df-csb 3895 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
107, 8, 93eqtr3i 2769 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
11 sbcel2gv 3850 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1211eqabcdv 2869 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1310, 12eqtrid 2785 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
141, 13syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  {cab 2710  Vcvv 3475  [wsbc 3778  csb 3894
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-sbc 3779  df-csb 3895
This theorem is referenced by:  csbvargi  4433  sbccsb2  4435  2nreu  4442  csbfv  6942  ixpsnval  8894  csbwrdg  14494  swrdspsleq  14615  prmgaplem7  16990  telgsums  19861  ixpsnbasval  20832  scmatscm  22015  pm2mpf1lem  22296  pm2mpcoe1  22302  idpm2idmp  22303  pm2mpmhmlem2  22321  monmat2matmon  22326  pm2mp  22327  fvmptnn04if  22351  chfacfscmulfsupp  22361  cayhamlem4  22390  divcncf  24964  opsbc2ie  31716  esum2dlem  33090  relowlpssretop  36245  rdgeqoa  36251  renegclALT  37833  cdlemk40  39788  tfsconcatfv  42091  iscard4  42284  minregex  42285  cotrclrcl  42493  frege124d  42512  frege70  42684  frege72  42686  frege77  42691  frege91  42705  frege92  42706  frege116  42730  frege118  42732  frege120  42734  rusbcALT  43198  onfrALTlem5  43303  onfrALTlem4  43304  onfrALTlem5VD  43646  iccelpart  46101  ply1mulgsumlem4  47070
  Copyright terms: Public domain W3C validator