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

Theorem r19.23v 2937
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 1674 . 2  |-  F/ x ps
21r19.23 2936 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wral 2798   E.wrex 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2803  df-rex 2804
This theorem is referenced by:  ralxpxfr2d  3189  uniiunlem  3547  dfiin2g  4310  iunss  4318  ralxfr2d  4615  ssrel2  5037  reliun  5067  funimass4  5850  ralrnmpt2  6314  kmlem12  8440  fimaxre3  10389  gcdcllem1  13812  vdwmc2  14157  iunocv  18230  islindf4  18391  ovolgelb  21094  dyadmax  21210  itg2leub  21344  mptelee  23292  nmoubi  24323  nmopub  25463  nmfnleub  25480  sigaclcu2  26707  untuni  27503  dfpo2  27708  heibor1lem  28855  2reu4a  30160  ispsubsp2  33713  pmapglbx  33736
  Copyright terms: Public domain W3C validator