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

Theorem csbeq2dv 3684
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 1678 . 2  |-  F/ x ph
2 csbeq2dv.1 . 2  |-  ( ph  ->  B  =  C )
31, 2csbeq2d 3683 1  |-  ( ph  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364   [_csb 3285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-sbc 3184  df-csb 3286
This theorem is referenced by:  csbeq2i  3685  mpt2mptsx  6636  dmmpt2ssx  6638  fmpt2x  6639  offval22  6651  ovmptss  6653  fmpt2co  6655  cantnffval  7865  fsumcom2  13237  ruclem1  13509  natfval  14852  fucval  14864  evlfval  15023  mpfrcl  17580  fsumcn  20405  fsum2cn  20406  dvmptfsum  21406  ttgval  23056  fprodcom2  27424  bpolylem  28120  bpolyval  28121  mpt2sn  30647  dmmpt2ssx2  30651  cdleme31sde  33751  cdlemeg47rv2  33876
  Copyright terms: Public domain W3C validator