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

Theorem ralbid 2888
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 463 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
41, 3ralbida 2887 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 1621    e. wcel 1823   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622  df-ral 2809
This theorem is referenced by:  ralbidvOLD  2894  raleqbid  3063  sbcralt  3397  sbcrext  3398  riota5f  6256  zfrep6  6741  cnfcom3clem  8140  cnfcom3clemOLD  8148  cplem2  8299  infxpenc2lem2  8388  infxpenc2lem2OLD  8392  acnlem  8420  lble  10490  fsuppmapnn0fiubex  12083  chirred  27515  aciunf1lem  27732  indexa  30467  climf  31870  cncficcgt0  31933  stoweidlem16  32040  stoweidlem18  32042  stoweidlem21  32045  stoweidlem29  32053  stoweidlem31  32055  stoweidlem36  32060  stoweidlem41  32065  stoweidlem44  32068  stoweidlem45  32069  stoweidlem51  32075  stoweidlem55  32079  stoweidlem59  32083  stoweidlem60  32084  riotasvd  35103  cdlemk36  37055
  Copyright terms: Public domain W3C validator