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

Theorem r19.23v 2814
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 2813 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wral 2697   E.wrex 2698
This theorem is referenced by:  uniiunlem  3423  dfiin2g  4116  iunss  4124  ralxfr2d  4730  ssrel2  4957  reliun  4986  funimass4  5768  ralrnmpt2  6175  kmlem12  8030  fimaxre3  9946  gcdcllem1  12999  vdwmc2  13335  iunocv  16896  ovolgelb  19364  dyadmax  19478  itg2leub  19614  nmoubi  22261  nmopub  23399  nmfnleub  23416  sigaclcu2  24491  untuni  25146  dfpo2  25367  mptelee  25782  heibor1lem  26455  ralxpxfr2d  26678  islindf4  27223  2reu4a  27881  ispsubsp2  30382  pmapglbx  30405
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator