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

Theorem csbeq2dv 3821
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  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
csbeq2dv  |-  ( ph  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )
Distinct variable group:    ph, x
Allowed substitution hints:    A( x)    B( x)    C( x)

Proof of Theorem csbeq2dv
StepHypRef Expression
1 nfv 1694 . 2  |-  F/ x ph
2 csbeq2dv.1 . 2  |-  ( ph  ->  B  =  C )
31, 2csbeq2d 3820 1  |-  ( ph  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   [_csb 3420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-sbc 3314  df-csb 3421
This theorem is referenced by:  csbeq2i  3822  mpt2mptsx  6848  dmmpt2ssx  6850  fmpt2x  6851  offval22  6864  ovmptss  6866  fmpt2co  6868  mpt2sn  6876  mpt2curryd  7000  fvmpt2curryd  7002  cantnffval  8083  fsumcom2  13568  ruclem1  13841  natfval  15189  fucval  15201  evlfval  15360  mpfrcl  18061  pmatcollpw3lem  19157  fsumcn  21247  fsum2cn  21248  dvmptfsum  22249  ttgval  24050  nbgraopALT  24296  msrfval  28770  fprodcom2  29089  bpolylem  29785  bpolyval  29786  rnghmval  32415  dmmpt2ssx2  32659  cdleme31sde  35851  cdlemeg47rv2  35976
  Copyright terms: Public domain W3C validator