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

Theorem csbeq2dv 3119
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 1609 . 2  |-  F/ x ph
2 csbeq2dv.1 . 2  |-  ( ph  ->  B  =  C )
31, 2csbeq2d 3118 1  |-  ( ph  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   [_csb 3094
This theorem is referenced by:  csbeq2i  3120  mpt2mptsx  6203  dmmpt2ssx  6205  fmpt2x  6206  ovmptss  6216  fmpt2co  6218  cantnffval  7380  fsumcom2  12253  ruclem1  12525  natfval  13836  fucval  13848  evlfval  14007  fsumcn  18390  fsum2cn  18391  dvmptfsum  19338  mpfrcl  19418  bpolylem  24855  bpolyval  24856  cdleme31sde  31196  cdlemeg47rv2  31321
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-sbc 3005  df-csb 3095
  Copyright terms: Public domain W3C validator