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

Theorem sbcbidv 3207
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 1629 . 2  |-  F/ x ph
2 sbcbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2sbcbid 3206 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  [. A  /  x ]. ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   [.wsbc 3153
This theorem is referenced by:  sbcbii  3208  csbcomg  3266  opelopabsb  4457  opelopabf  4471  fpwwe2cbv  8497  fpwwe2lem2  8499  fpwwe2lem3  8500  isprs  14379  isdrs  14383  istos  14456  isdlat  14611  islmod  15946  elmptrab  17851  isofld  24227  indexa  26426  sdclem2  26437  sdclem1  26438  fdc  26440  sbccomieg  26840  rexrabdioph  26845  rexfrabdioph  26846  2rexfrabdioph  26847  3rexfrabdioph  26848  4rexfrabdioph  26849  6rexfrabdioph  26850  7rexfrabdioph  26851  2sbc6g  27583  2sbc5g  27584  hdmap1ffval  32531  hdmap1fval  32532  hdmapffval  32564  hdmapfval  32565  hgmapffval  32623  hgmapfval  32624
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-sbc 3154
  Copyright terms: Public domain W3C validator