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

Theorem sbcbidv 3159
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 1626 . 2  |-  F/ x ph
2 sbcbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2sbcbid 3158 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  [. A  /  x ]. ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   [.wsbc 3105
This theorem is referenced by:  sbcbii  3160  csbcomg  3218  opelopabsb  4407  opelopabf  4421  fpwwe2cbv  8439  fpwwe2lem2  8441  fpwwe2lem3  8442  isprs  14315  isdrs  14319  istos  14392  isdlat  14547  islmod  15882  elmptrab  17781  isofld  24062  indexa  26127  sdclem2  26138  sdclem1  26139  fdc  26141  sbccomieg  26541  rexrabdioph  26546  rexfrabdioph  26547  2rexfrabdioph  26548  3rexfrabdioph  26549  4rexfrabdioph  26550  6rexfrabdioph  26551  7rexfrabdioph  26552  2sbc6g  27285  2sbc5g  27286  hdmap1ffval  31912  hdmap1fval  31913  hdmapffval  31945  hdmapfval  31946  hgmapffval  32004  hgmapfval  32005
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-sbc 3106
  Copyright terms: Public domain W3C validator