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

Theorem csbeq2dv 3915
Description: Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
Hypothesis
Ref Expression
csbeq2dv.1 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
csbeq2dv (𝜑𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem csbeq2dv
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 csbeq2dv.1 . . . . 5 (𝜑𝐵 = 𝐶)
21eleq2d 2825 . . . 4 (𝜑 → (𝑦𝐵𝑦𝐶))
32sbcbidv 3851 . . 3 (𝜑 → ([𝐴 / 𝑥]𝑦𝐵[𝐴 / 𝑥]𝑦𝐶))
43abbidv 2806 . 2 (𝜑 → {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐶})
5 df-csb 3909 . 2 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
6 df-csb 3909 . 2 𝐴 / 𝑥𝐶 = {𝑦[𝐴 / 𝑥]𝑦𝐶}
74, 5, 63eqtr4g 2800 1 (𝜑𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wcel 2106  {cab 2712  [wsbc 3791  csb 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792  df-csb 3909
This theorem is referenced by:  csbeq2i  3916  csbeq12dv  3917  mpomptsx  8088  dmmpossx  8090  fmpox  8091  el2mpocsbcl  8109  offval22  8112  ovmptss  8117  fmpoco  8119  mposn  8127  mpocurryd  8293  fvmpocurryd  8295  cantnffval  9701  sumeq2sdv  15736  fsumcom2  15807  prodeq2sdv  15956  fprodcom2  16017  bpolylem  16081  bpolyval  16082  ruclem1  16264  natfval  18001  fucval  18014  evlfval  18274  rnghmval  20457  mpfrcl  22127  selvffval  22155  selvfval  22156  selvval  22157  pmatcollpw3lem  22805  fsumcn  24908  fsum2cn  24909  itgeq1f  25821  itgeq1  25823  dvmptfsum  26028  mulsval  28150  precsexlemcbv  28245  ttgvalOLD  28899  msrfval  35522  poimirlem5  37612  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem15  37622  poimirlem18  37625  poimirlem21  37628  poimirlem22  37629  poimirlem24  37631  poimirlem26  37633  poimirlem27  37634  cdleme31sde  40368  cdlemeg47rv2  40493  dmmpossx2  48182
  Copyright terms: Public domain W3C validator