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

Theorem r19.23v 2672
Description: Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 31-Aug-1999.)
Assertion
Ref Expression
r19.23v  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem r19.23v
StepHypRef Expression
1 nfv 1609 . 2  |-  F/ x ps
21r19.23 2671 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wral 2556   E.wrex 2557
This theorem is referenced by:  uniiunlem  3273  dfiin2g  3952  iunss  3959  ralxfr2d  4566  reliun  4822  funimass4  5589  ralrnmpt2  5974  kmlem12  7803  fimaxre3  9719  gcdcllem1  12706  vdwmc2  13042  iunocv  16597  ovolgelb  18855  dyadmax  18969  itg2leub  19105  nmoubi  21366  nmopub  22504  nmfnleub  22521  esumcvg  23469  sigaclcu2  23496  untuni  24070  dfpo2  24183  mptelee  24595  heibor1lem  26636  ralxpxfr2d  26863  islindf4  27411  2reu4a  28070  ispsubsp2  30557  pmapglbx  30580
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-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator