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

Theorem csbeq2dv 3944
Description: Formula-building deduction rule 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 1830 . 2 𝑥𝜑
2 csbeq2dv.1 . 2 (𝜑𝐵 = 𝐶)
31, 2csbeq2d 3943 1 (𝜑𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  csb 3499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sbc 3403  df-csb 3500
This theorem is referenced by:  csbeq2i  3945  mpt2mptsx  7122  dmmpt2ssx  7124  fmpt2x  7125  el2mpt2csbcl  7137  offval22  7140  ovmptss  7145  fmpt2co  7147  mpt2sn  7155  mpt2curryd  7282  fvmpt2curryd  7284  cantnffval  8443  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  bpolylem  14618  bpolyval  14619  ruclem1  14799  natfval  16429  fucval  16441  evlfval  16680  mpfrcl  19339  pmatcollpw3lem  20407  fsumcn  22481  fsum2cn  22482  dvmptfsum  23542  ttgval  25555  nbgraopALT  25953  msrfval  30688  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem24  32603  poimirlem26  32605  poimirlem27  32606  cdleme31sde  34691  cdlemeg47rv2  34816  rnghmval  41681  dmmpt2ssx2  41908
  Copyright terms: Public domain W3C validator