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

Theorem csbeq2dv 3896
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
StepHypRef Expression
1 nfv 1910 . 2 𝑥𝜑
2 csbeq2dv.1 . 2 (𝜑𝐵 = 𝐶)
31, 2csbeq2d 3895 1 (𝜑𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1534  csb 3889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-12 2164  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-sbc 3775  df-csb 3890
This theorem is referenced by:  csbeq2i  3897  csbeq12dv  3898  mpomptsx  8062  dmmpossx  8064  fmpox  8065  el2mpocsbcl  8084  offval22  8087  ovmptss  8092  fmpoco  8094  mposn  8102  mpocurryd  8268  fvmpocurryd  8270  cantnffval  9678  fsumcom2  15744  fprodcom2  15952  bpolylem  16016  bpolyval  16017  ruclem1  16199  natfval  17927  fucval  17940  evlfval  18200  rnghmval  20368  mpfrcl  22018  selvffval  22046  selvfval  22047  selvval  22048  pmatcollpw3lem  22672  fsumcn  24775  fsum2cn  24776  dvmptfsum  25894  mulsval  27996  precsexlemcbv  28091  ttgvalOLD  28667  msrfval  35083  poimirlem5  37033  poimirlem6  37034  poimirlem7  37035  poimirlem8  37036  poimirlem10  37038  poimirlem11  37039  poimirlem12  37040  poimirlem15  37043  poimirlem18  37046  poimirlem21  37049  poimirlem22  37050  poimirlem24  37052  poimirlem26  37054  poimirlem27  37055  cdleme31sde  39795  cdlemeg47rv2  39920  dmmpossx2  47323
  Copyright terms: Public domain W3C validator