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

Theorem sbcbidv 3353
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 1674 . 2  |-  F/ x ph
2 sbcbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2sbcbid 3352 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  [. A  /  x ]. ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   [.wsbc 3294
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3295
This theorem is referenced by:  sbcbii  3354  csbcomgOLD  3799  opelopabsb  4708  opelopabf  4722  sbcfng  5665  sbcfg  5666  fpwwe2cbv  8909  fpwwe2lem2  8911  fpwwe2lem3  8912  wrd2ind  12491  isprs  15220  isdrs  15224  istos  15325  isdlat  15483  islmod  17076  elmptrab  19533  f1od2  26176  isomnd  26310  isorng  26413  indexa  28776  sdclem2  28787  sdclem1  28788  fdc  28790  sbcalf  29069  sbcexf  29070  sbccomieg  29280  rexrabdioph  29281  rexfrabdioph  29282  2rexfrabdioph  29283  3rexfrabdioph  29284  4rexfrabdioph  29285  6rexfrabdioph  29286  7rexfrabdioph  29287  2sbc6g  29818  2sbc5g  29819  opelopabgf  30285  fmptsnd  30871  hdmap1ffval  35780  hdmap1fval  35781  hdmapffval  35813  hdmapfval  35814  hgmapffval  35872  hgmapfval  35873
  Copyright terms: Public domain W3C validator