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

Theorem r19.23v 2621
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 1629 . 2  |-  F/ x ps
21r19.23 2620 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 2509   E.wrex 2510
This theorem is referenced by:  uniiunlem  3181  dfiin2g  3834  iunss  3841  ralxfr2d  4441  reliun  4713  funimass4  5425  ralrnmpt2  5810  kmlem12  7671  fimaxre3  9583  gcdcllem1  12564  vdwmc2  12900  iunocv  16413  ovolgelb  18671  dyadmax  18785  itg2leub  18921  nmoubi  21180  nmopub  22318  nmfnleub  22335  untuni  23226  dfpo2  23282  mptelee  23697  heibor1lem  25699  ralxpxfr2d  25926  islindf4  26474  ispsubsp2  28624  pmapglbx  28647
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
  Copyright terms: Public domain W3C validator