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

Theorem ralbid 2574
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 2570 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 1534    e. wcel 1696   A.wral 2556
This theorem is referenced by:  ralbidv  2576  sbcralt  3076  sbcrext  3077  zfrep6  5764  riota5f  6345  riotasvd  6363  riotasvdOLD  6364  cnfcom3clem  7424  cplem2  7576  infxpenc2lem2  7663  acnlem  7691  lble  9722  chirred  22991  raleqbid  23147  svli2  25587  intopcoaconb  25643  indexa  26515  evth2f  27789  stoweidlem16  27868  stoweidlem18  27870  stoweidlem21  27873  stoweidlem29  27881  stoweidlem31  27883  stoweidlem36  27888  stoweidlem41  27893  stoweidlem44  27896  stoweidlem45  27897  stoweidlem51  27903  stoweidlem55  27907  stoweidlem59  27911  stoweidlem60  27912  cdlemk36  31724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator