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

Theorem csbvarg 4147
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 3364 . 2 (𝐴𝑉𝐴 ∈ V)
2 vex 3354 . . . . . 6 𝑦 ∈ V
3 df-csb 3683 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
4 sbcel2gv 3647 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
54abbi1dv 2892 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
63, 5syl5eq 2817 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
72, 6ax-mp 5 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
87csbeq2i 4137 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
9 csbco 3692 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
10 df-csb 3683 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
118, 9, 103eqtr3i 2801 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
12 sbcel2gv 3647 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1312abbi1dv 2892 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1411, 13syl5eq 2817 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
151, 14syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145  {cab 2757  Vcvv 3351  [wsbc 3587  csb 3682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353  df-sbc 3588  df-csb 3683
This theorem is referenced by:  sbccsb2  4149  csbfv  6372  ixpsnval  8063  csbwrdg  13523  swrdspsleq  13651  prmgaplem7  15961  telgsums  18591  ixpsnbasval  19417  scmatscm  20530  pm2mpf1lem  20812  pm2mpcoe1  20818  idpm2idmp  20819  pm2mpmhmlem2  20837  monmat2matmon  20842  pm2mp  20843  fvmptnn04if  20867  chfacfscmulfsupp  20877  cayhamlem4  20906  divcncf  23428  iuninc  29710  f1od2  29832  esum2dlem  30487  bnj110  31259  bj-sels  33274  relowlpssretop  33542  rdgeqoa  33548  finxpreclem4  33561  csbvargi  34246  renegclALT  34764  cdlemk40  36719  brtrclfv2  38538  cotrclrcl  38553  frege124d  38572  frege70  38746  frege72  38748  frege77  38753  frege91  38767  frege92  38768  frege116  38792  frege118  38794  frege120  38796  rusbcALT  39159  onfrALTlem5  39275  onfrALTlem4  39276  onfrALTlem5VD  39636  onfrALTlem4VD  39637  iccelpart  41890  ply1mulgsumlem4  42698
  Copyright terms: Public domain W3C validator