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

Theorem csbeq2dv 3106
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 1605 . 2  |-  F/ x ph
2 csbeq2dv.1 . 2  |-  ( ph  ->  B  =  C )
31, 2csbeq2d 3105 1  |-  ( ph  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   [_csb 3081
This theorem is referenced by:  csbeq2i  3107  mpt2mptsx  6187  dmmpt2ssx  6189  fmpt2x  6190  ovmptss  6200  fmpt2co  6202  cantnffval  7364  fsumcom2  12237  ruclem1  12509  natfval  13820  fucval  13832  evlfval  13991  fsumcn  18374  fsum2cn  18375  dvmptfsum  19322  mpfrcl  19402  bpolylem  24783  bpolyval  24784  cdleme31sde  30574  cdlemeg47rv2  30699
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-sbc 2992  df-csb 3082
  Copyright terms: Public domain W3C validator