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

Theorem csbvarg 4380
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 3510 . 2 (𝐴𝑉𝐴 ∈ V)
2 df-csb 3881 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
3 sbcel2gv 3838 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
43abbi1dv 2949 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
52, 4syl5eq 2865 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
65elv 3497 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
76csbeq2i 3888 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
8 csbcow 3895 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
9 df-csb 3881 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
107, 8, 93eqtr3i 2849 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
11 sbcel2gv 3838 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1211abbi1dv 2949 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1310, 12syl5eq 2865 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
141, 13syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  {cab 2796  Vcvv 3492  [wsbc 3769  csb 3880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-v 3494  df-sbc 3770  df-csb 3881
This theorem is referenced by:  csbvargi  4381  sbccsb2  4383  2nreu  4389  csbfv  6708  ixpsnval  8452  csbwrdg  13883  swrdspsleq  14015  prmgaplem7  16381  telgsums  19042  ixpsnbasval  19910  scmatscm  21050  pm2mpf1lem  21330  pm2mpcoe1  21336  idpm2idmp  21337  pm2mpmhmlem2  21355  monmat2matmon  21360  pm2mp  21361  fvmptnn04if  21385  chfacfscmulfsupp  21395  cayhamlem4  21424  divcncf  23975  opsbc2ie  30166  esum2dlem  31250  relowlpssretop  34527  rdgeqoa  34533  renegclALT  35979  cdlemk40  37933  iscard4  39778  cotrclrcl  39965  frege124d  39984  frege70  40157  frege72  40159  frege77  40164  frege91  40178  frege92  40179  frege116  40203  frege118  40205  frege120  40207  rusbcALT  40648  onfrALTlem5  40753  onfrALTlem4  40754  onfrALTlem5VD  41096  iccelpart  43470  ply1mulgsumlem4  44371
  Copyright terms: Public domain W3C validator