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

Theorem ralbid 2725
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 453 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
41, 3ralbida 2721 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   F/wnf 1554    e. wcel 1726   A.wral 2707
This theorem is referenced by:  ralbidv  2727  sbcralt  3235  sbcrext  3236  zfrep6  5970  riota5f  6576  riotasvd  6594  riotasvdOLD  6595  cnfcom3clem  7664  cplem2  7816  infxpenc2lem2  7903  acnlem  7931  lble  9962  chirred  23900  raleqbid  23965  indexa  26437  stoweidlem16  27743  stoweidlem18  27745  stoweidlem21  27748  stoweidlem29  27756  stoweidlem31  27758  stoweidlem36  27763  stoweidlem41  27768  stoweidlem44  27771  stoweidlem45  27772  stoweidlem51  27778  stoweidlem55  27782  stoweidlem59  27786  stoweidlem60  27787  cdlemk36  31772
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2712
  Copyright terms: Public domain W3C validator