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

Theorem csbvarg 4434
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 3501 . 2 (𝐴𝑉𝐴 ∈ V)
2 df-csb 3900 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
3 sbcel2gv 3857 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
43eqabcdv 2876 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
52, 4eqtrid 2789 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
65elv 3485 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
76csbeq2i 3907 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
8 csbcow 3914 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
9 df-csb 3900 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
107, 8, 93eqtr3i 2773 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
11 sbcel2gv 3857 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1211eqabcdv 2876 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1310, 12eqtrid 2789 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
141, 13syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108  {cab 2714  Vcvv 3480  [wsbc 3788  csb 3899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-sbc 3789  df-csb 3900
This theorem is referenced by:  csbvargi  4435  sbccsb2  4437  2nreu  4444  csbfv  6956  ixpsnval  8940  csbwrdg  14582  swrdspsleq  14703  prmgaplem7  17095  telgsums  20011  ixpsnbasval  21215  scmatscm  22519  pm2mpf1lem  22800  pm2mpcoe1  22806  idpm2idmp  22807  pm2mpmhmlem2  22825  monmat2matmon  22830  pm2mp  22831  fvmptnn04if  22855  chfacfscmulfsupp  22865  cayhamlem4  22894  divcncf  25482  opsbc2ie  32495  esum2dlem  34093  relowlpssretop  37365  rdgeqoa  37371  renegclALT  38964  cdlemk40  40919  tfsconcatfv  43354  iscard4  43546  minregex  43547  cotrclrcl  43755  frege124d  43774  frege70  43946  frege72  43948  frege77  43953  frege91  43967  frege92  43968  frege116  43992  frege118  43994  frege120  43996  rusbcALT  44458  onfrALTlem5  44562  onfrALTlem4  44563  onfrALTlem5VD  44905  iccelpart  47420  ply1mulgsumlem4  48306
  Copyright terms: Public domain W3C validator