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

Theorem csbeq2dv 3754
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 1755 . 2  |-  F/ x ph
2 csbeq2dv.1 . 2  |-  ( ph  ->  B  =  C )
31, 2csbeq2d 3753 1  |-  ( ph  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   [_csb 3338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-sbc 3243  df-csb 3339
This theorem is referenced by:  csbeq2i  3755  mpt2mptsx  6814  dmmpt2ssx  6816  fmpt2x  6817  offval22  6830  ovmptss  6832  fmpt2co  6834  mpt2sn  6842  mpt2curryd  6971  fvmpt2curryd  6973  cantnffval  8120  fsumcom2  13778  fprodcom2  13981  bpolylem  14044  bpolyval  14045  ruclem1  14226  natfval  15794  fucval  15806  evlfval  16045  mpfrcl  18684  pmatcollpw3lem  19749  fsumcn  21844  fsum2cn  21845  dvmptfsum  22869  ttgval  24847  nbgraopALT  25094  msrfval  30127  poimirlem5  31852  poimirlem6  31853  poimirlem7  31854  poimirlem8  31855  poimirlem10  31857  poimirlem11  31858  poimirlem12  31859  poimirlem15  31862  poimirlem16  31863  poimirlem17  31864  poimirlem18  31865  poimirlem19  31866  poimirlem20  31867  poimirlem21  31868  poimirlem22  31869  poimirlem24  31871  poimirlem26  31873  poimirlem27  31874  cdleme31sde  33864  cdlemeg47rv2  33989  rnghmval  39492  dmmpt2ssx2  39721
  Copyright terms: Public domain W3C validator