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

Theorem csbeq2dv 3873
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 1916 . 2 𝑥𝜑
2 csbeq2dv.1 . 2 (𝜑𝐵 = 𝐶)
31, 2csbeq2d 3872 1 (𝜑𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  csb 3866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-sbc 3759  df-csb 3867
This theorem is referenced by:  csbeq2i  3874  csbeq12dv  3875  mpomptsx  7757  dmmpossx  7759  fmpox  7760  el2mpocsbcl  7776  offval22  7779  ovmptss  7784  fmpoco  7786  mposn  7794  mpocurryd  7931  fvmpocurryd  7933  cantnffval  9123  fsumcom2  15129  fprodcom2  15338  bpolylem  15402  bpolyval  15403  ruclem1  15584  natfval  17216  fucval  17228  evlfval  17467  mpfrcl  20298  selvffval  20329  selvfval  20330  selvval  20331  pmatcollpw3lem  21391  fsumcn  23478  fsum2cn  23479  dvmptfsum  24581  ttgval  26672  msrfval  32841  poimirlem5  35007  poimirlem6  35008  poimirlem7  35009  poimirlem8  35010  poimirlem10  35012  poimirlem11  35013  poimirlem12  35014  poimirlem15  35017  poimirlem16  35018  poimirlem17  35019  poimirlem18  35020  poimirlem19  35021  poimirlem20  35022  poimirlem21  35023  poimirlem22  35024  poimirlem24  35026  poimirlem26  35028  poimirlem27  35029  cdleme31sde  37626  cdlemeg47rv2  37751  rnghmval  44441  dmmpossx2  44664
  Copyright terms: Public domain W3C validator