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

Theorem csbeq2dv 3831
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 1712 . 2  |-  F/ x ph
2 csbeq2dv.1 . 2  |-  ( ph  ->  B  =  C )
31, 2csbeq2d 3830 1  |-  ( ph  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398   [_csb 3420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3325  df-csb 3421
This theorem is referenced by:  csbeq2i  3832  mpt2mptsx  6836  dmmpt2ssx  6838  fmpt2x  6839  offval22  6852  ovmptss  6854  fmpt2co  6856  mpt2sn  6864  mpt2curryd  6990  fvmpt2curryd  6992  cantnffval  8071  fsumcom2  13671  fprodcom2  13870  ruclem1  14048  natfval  15434  fucval  15446  evlfval  15685  mpfrcl  18382  pmatcollpw3lem  19451  fsumcn  21540  fsum2cn  21541  dvmptfsum  22542  ttgval  24380  nbgraopALT  24626  msrfval  29161  bpolylem  30038  bpolyval  30039  rnghmval  32951  dmmpt2ssx2  33180  cdleme31sde  36508  cdlemeg47rv2  36633
  Copyright terms: Public domain W3C validator