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

Theorem ralbid 2813
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)
Hypotheses
Ref Expression
ralbid.1  |-  F/ x ph
ralbid.2  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
ralbid  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)

Proof of Theorem ralbid
StepHypRef Expression
1 ralbid.1 . 2  |-  F/ x ph
2 ralbid.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32adantr 465 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
41, 3ralbida 2809 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   F/wnf 1590    e. wcel 1757   A.wral 2792
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 1709  ax-7 1729  ax-12 1793
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2797
This theorem is referenced by:  ralbidv  2815  raleqbid  3011  sbcralt  3351  sbcrextOLD  3352  sbcrext  3353  riota5f  6162  zfrep6  6631  cnfcom3clem  8025  cnfcom3clemOLD  8033  cplem2  8184  infxpenc2lem2  8273  infxpenc2lem2OLD  8277  acnlem  8305  lble  10369  chirred  25920  indexa  28751  stoweidlem16  29935  stoweidlem18  29937  stoweidlem21  29940  stoweidlem29  29948  stoweidlem31  29950  stoweidlem36  29955  stoweidlem41  29960  stoweidlem44  29963  stoweidlem45  29964  stoweidlem51  29970  stoweidlem55  29974  stoweidlem59  29978  stoweidlem60  29979  fsuppmapnn0fiubex  30924  riotasvd  32889  cdlemk36  34839
  Copyright terms: Public domain W3C validator