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

Theorem ralbid 2898
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 2897 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 1599    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-ral 2819
This theorem is referenced by:  ralbidvOLD  2904  raleqbid  3070  sbcralt  3412  sbcrextOLD  3413  sbcrext  3414  riota5f  6268  zfrep6  6749  cnfcom3clem  8145  cnfcom3clemOLD  8153  cplem2  8304  infxpenc2lem2  8393  infxpenc2lem2OLD  8397  acnlem  8425  lble  10491  fsuppmapnn0fiubex  12062  chirred  26990  indexa  29827  mullimc  31158  climf  31164  mullimcf  31165  cncficcgt0  31227  stoweidlem16  31316  stoweidlem18  31318  stoweidlem21  31321  stoweidlem29  31329  stoweidlem31  31331  stoweidlem36  31336  stoweidlem41  31341  stoweidlem44  31344  stoweidlem45  31345  stoweidlem51  31351  stoweidlem55  31355  stoweidlem59  31359  stoweidlem60  31360  riotasvd  33759  cdlemk36  35709
  Copyright terms: Public domain W3C validator