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

Theorem csbvarg 4144
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 3350 . 2 (𝐴𝑉𝐴 ∈ V)
2 vex 3341 . . . . . 6 𝑦 ∈ V
3 df-csb 3673 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
4 sbcel2gv 3635 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
54abbi1dv 2879 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
63, 5syl5eq 2804 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
72, 6ax-mp 5 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
87csbeq2i 4134 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
9 csbco 3682 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
10 df-csb 3673 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
118, 9, 103eqtr3i 2788 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
12 sbcel2gv 3635 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1312abbi1dv 2879 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1411, 13syl5eq 2804 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
151, 14syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  wcel 2137  {cab 2744  Vcvv 3338  [wsbc 3574  csb 3672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-v 3340  df-sbc 3575  df-csb 3673
This theorem is referenced by:  sbccsb2  4146  csbfv  6392  ixpsnval  8075  csbwrdg  13518  swrdspsleq  13647  prmgaplem7  15961  telgsums  18588  ixpsnbasval  19409  scmatscm  20519  pm2mpf1lem  20799  pm2mpcoe1  20805  idpm2idmp  20806  pm2mpmhmlem2  20824  monmat2matmon  20829  pm2mp  20830  fvmptnn04if  20854  chfacfscmulfsupp  20864  cayhamlem4  20893  divcncf  23414  iuninc  29684  f1od2  29806  esum2dlem  30461  bnj110  31233  bj-sels  33254  relowlpssretop  33521  rdgeqoa  33527  finxpreclem4  33540  csbvargi  34232  renegclALT  34750  cdlemk40  36705  brtrclfv2  38519  cotrclrcl  38534  frege124d  38553  frege70  38727  frege72  38729  frege77  38734  frege91  38748  frege92  38749  frege116  38773  frege118  38775  frege120  38777  rusbcALT  39140  onfrALTlem5  39257  onfrALTlem4  39258  onfrALTlem5VD  39618  onfrALTlem4VD  39619  iccelpart  41877  ply1mulgsumlem4  42685
  Copyright terms: Public domain W3C validator