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

Theorem sbcbidv 3379
Description: Formula-building deduction rule for class substitution. (Contributed by NM, 29-Dec-2014.)
Hypothesis
Ref Expression
sbcbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
sbcbidv  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  [. A  /  x ]. ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem sbcbidv
StepHypRef Expression
1 nfv 1712 . 2  |-  F/ x ph
2 sbcbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2sbcbid 3378 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  [. A  /  x ]. ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   [.wsbc 3324
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
This theorem is referenced by:  sbcbii  3380  opelopabsb  4746  opelopabgf  4756  opelopabf  4761  sbcfng  5710  sbcfg  5711  fmptsnd  6069  wrd2ind  12694  islmod  17711  elmptrab  20494  nbgraopALT  24626  f1od2  27778  isomnd  27925  isorng  28024  indexa  30464  sdclem2  30475  sdclem1  30476  fdc  30478  sbcalf  30757  sbcexf  30758  rexrabdioph  30967  rexfrabdioph  30968  2rexfrabdioph  30969  3rexfrabdioph  30970  4rexfrabdioph  30971  6rexfrabdioph  30972  7rexfrabdioph  30973  2sbc6g  31563  2sbc5g  31564  hdmap1ffval  37920  hdmap1fval  37921  hdmapffval  37953  hdmapfval  37954  hgmapffval  38012  hgmapfval  38013
  Copyright terms: Public domain W3C validator