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

Theorem sbcbidv 3370
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 1692 . 2  |-  F/ x ph
2 sbcbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2sbcbid 3369 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  [. A  /  x ]. ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   [.wsbc 3311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-sbc 3312
This theorem is referenced by:  sbcbii  3371  csbcomgOLD  3820  opelopabsb  4743  opelopabgf  4753  opelopabf  4758  sbcfng  5714  sbcfg  5715  fmptsnd  6074  wrd2ind  12677  islmod  17384  elmptrab  20194  nbgraopALT  24289  f1od2  27412  isomnd  27557  isorng  27655  indexa  30192  sdclem2  30203  sdclem1  30204  fdc  30206  sbcalf  30485  sbcexf  30486  rexrabdioph  30695  rexfrabdioph  30696  2rexfrabdioph  30697  3rexfrabdioph  30698  4rexfrabdioph  30699  6rexfrabdioph  30700  7rexfrabdioph  30701  2sbc6g  31269  2sbc5g  31270  hdmap1ffval  37225  hdmap1fval  37226  hdmapffval  37258  hdmapfval  37259  hgmapffval  37317  hgmapfval  37318
  Copyright terms: Public domain W3C validator