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

Theorem sbcbidv 3383
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 1678 . 2  |-  F/ x ph
2 sbcbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2sbcbid 3382 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 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-sbc 3325
This theorem is referenced by:  sbcbii  3384  csbcomgOLD  3831  opelopabsb  4750  opelopabgf  4760  opelopabf  4765  sbcfng  5719  sbcfg  5720  fmptsnd  6074  fpwwe2cbv  8997  fpwwe2lem2  8999  fpwwe2lem3  9000  wrd2ind  12653  isprs  15406  isdrs  15410  istos  15511  isdlat  15669  islmod  17292  elmptrab  20056  nbgraopALT  24086  f1od2  27205  isomnd  27339  isorng  27438  indexa  29814  sdclem2  29825  sdclem1  29826  fdc  29828  sbcalf  30107  sbcexf  30108  sbccomieg  30317  rexrabdioph  30318  rexfrabdioph  30319  2rexfrabdioph  30320  3rexfrabdioph  30321  4rexfrabdioph  30322  6rexfrabdioph  30323  7rexfrabdioph  30324  2sbc6g  30855  2sbc5g  30856  hdmap1ffval  36468  hdmap1fval  36469  hdmapffval  36501  hdmapfval  36502  hgmapffval  36560  hgmapfval  36561
  Copyright terms: Public domain W3C validator