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

Theorem ralbid 2561
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 451 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
41, 3ralbida 2557 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   F/wnf 1531    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralbidv  2563  sbcralt  3063  sbcrext  3064  zfrep6  5748  riota5f  6329  riotasvd  6347  riotasvdOLD  6348  cnfcom3clem  7408  cplem2  7560  infxpenc2lem2  7647  acnlem  7675  lble  9706  chirred  22975  raleqbid  23131  svli2  25484  intopcoaconb  25540  indexa  26412  evth2f  27686  stoweidlem16  27765  stoweidlem18  27767  stoweidlem21  27770  stoweidlem29  27778  stoweidlem31  27780  stoweidlem36  27785  stoweidlem41  27790  stoweidlem44  27793  stoweidlem45  27794  stoweidlem51  27800  stoweidlem55  27804  stoweidlem59  27808  stoweidlem60  27809  cdlemk36  31102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator