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

Theorem csbeq2dv 3828
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 3827 1  |-  ( ph  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374   [_csb 3428
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 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-sbc 3325  df-csb 3429
This theorem is referenced by:  csbeq2i  3829  mpt2mptsx  6837  dmmpt2ssx  6839  fmpt2x  6840  offval22  6852  ovmptss  6854  fmpt2co  6856  mpt2sn  6864  mpt2curryd  6988  fvmpt2curryd  6990  cantnffval  8069  fsumcom2  13538  ruclem1  13814  natfval  15162  fucval  15174  evlfval  15333  mpfrcl  17951  pmatcollpw3lem  19044  fsumcn  21102  fsum2cn  21103  dvmptfsum  22104  ttgval  23847  nbgraopALT  24086  fprodcom2  28677  bpolylem  29373  bpolyval  29374  dmmpt2ssx2  31865  cdleme31sde  35056  cdlemeg47rv2  35181
  Copyright terms: Public domain W3C validator