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

Theorem r19.23v 2634
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 2633 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 2518   E.wrex 2519
This theorem is referenced by:  uniiunlem  3235  dfiin2g  3910  iunss  3917  ralxfr2d  4522  reliun  4794  funimass4  5507  ralrnmpt2  5892  kmlem12  7755  fimaxre3  9671  gcdcllem1  12652  vdwmc2  12988  iunocv  16543  ovolgelb  18801  dyadmax  18915  itg2leub  19051  nmoubi  21310  nmopub  22448  nmfnleub  22465  untuni  23427  dfpo2  23483  mptelee  23898  heibor1lem  25900  ralxpxfr2d  26127  islindf4  26675  ispsubsp2  29102  pmapglbx  29125
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 2523  df-rex 2524
  Copyright terms: Public domain W3C validator