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

Theorem r19.23v 2660
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 1610 . 2  |-  F/ x ps
21r19.23 2659 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   A.wral 2544   E.wrex 2545
This theorem is referenced by:  uniiunlem  3261  dfiin2g  3937  iunss  3944  ralxfr2d  4549  reliun  4805  funimass4  5534  ralrnmpt2  5919  kmlem12  7782  fimaxre3  9698  gcdcllem1  12684  vdwmc2  13020  iunocv  16575  ovolgelb  18833  dyadmax  18947  itg2leub  19083  nmoubi  21342  nmopub  22480  nmfnleub  22497  untuni  23459  dfpo2  23515  mptelee  23930  heibor1lem  25932  ralxpxfr2d  26159  islindf4  26707  2reu4a  27346  ispsubsp2  29202  pmapglbx  29225
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-11 1719
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1534  df-nf 1537  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator