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

Theorem csbvarg 3980
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 3201 . 2 (𝐴𝑉𝐴 ∈ V)
2 vex 3192 . . . . . 6 𝑦 ∈ V
3 df-csb 3519 . . . . . . 7 𝑦 / 𝑥𝑥 = {𝑧[𝑦 / 𝑥]𝑧𝑥}
4 sbcel2gv 3482 . . . . . . . 8 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧𝑥𝑧𝑦))
54abbi1dv 2740 . . . . . . 7 (𝑦 ∈ V → {𝑧[𝑦 / 𝑥]𝑧𝑥} = 𝑦)
63, 5syl5eq 2667 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
72, 6ax-mp 5 . . . . 5 𝑦 / 𝑥𝑥 = 𝑦
87csbeq2i 3970 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑦𝑦
9 csbco 3528 . . . 4 𝐴 / 𝑦𝑦 / 𝑥𝑥 = 𝐴 / 𝑥𝑥
10 df-csb 3519 . . . 4 𝐴 / 𝑦𝑦 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
118, 9, 103eqtr3i 2651 . . 3 𝐴 / 𝑥𝑥 = {𝑧[𝐴 / 𝑦]𝑧𝑦}
12 sbcel2gv 3482 . . . 4 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧𝑦𝑧𝐴))
1312abbi1dv 2740 . . 3 (𝐴 ∈ V → {𝑧[𝐴 / 𝑦]𝑧𝑦} = 𝐴)
1411, 13syl5eq 2667 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝑥 = 𝐴)
151, 14syl 17 1 (𝐴𝑉𝐴 / 𝑥𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  {cab 2607  Vcvv 3189  [wsbc 3421  csb 3518
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3191  df-sbc 3422  df-csb 3519
This theorem is referenced by:  sbccsb2  3982  csbfv  6195  ixpsnval  7862  csbwrdg  13280  swrdspsleq  13394  prmgaplem7  15692  telgsums  18318  ixpsnbasval  19137  scmatscm  20247  pm2mpf1lem  20527  pm2mpcoe1  20533  idpm2idmp  20534  pm2mpmhmlem2  20552  monmat2matmon  20557  pm2mp  20558  fvmptnn04if  20582  chfacfscmulfsupp  20592  cayhamlem4  20621  divcncf  23135  iuninc  29242  f1od2  29360  esum2dlem  29953  bnj110  30663  bj-sels  32624  relowlpssretop  32871  rdgeqoa  32877  finxpreclem4  32890  csbvargi  33580  renegclALT  33756  cdlemk40  35712  brtrclfv2  37527  cotrclrcl  37542  frege124d  37561  frege70  37736  frege72  37738  frege77  37743  frege91  37757  frege92  37758  frege116  37782  frege118  37784  frege120  37786  rusbcALT  38149  onfrALTlem5  38266  onfrALTlem4  38267  onfrALTlem5VD  38631  onfrALTlem4VD  38632  iccelpart  40688  ply1mulgsumlem4  41486
  Copyright terms: Public domain W3C validator