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

Theorem r19.23v 2828
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 1673 . 2  |-  F/ x ps
21r19.23 2827 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 2710   E.wrex 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2715  df-rex 2716
This theorem is referenced by:  ralxpxfr2d  3079  uniiunlem  3435  dfiin2g  4198  iunss  4206  ralxfr2d  4503  ssrel2  4925  reliun  4955  funimass4  5737  ralrnmpt2  6200  kmlem12  8322  fimaxre3  10271  gcdcllem1  13687  vdwmc2  14032  iunocv  18081  islindf4  18242  ovolgelb  20938  dyadmax  21053  itg2leub  21187  mptelee  23092  nmoubi  24123  nmopub  25263  nmfnleub  25280  sigaclcu2  26515  untuni  27311  dfpo2  27516  heibor1lem  28661  2reu4a  29966  ispsubsp2  33230  pmapglbx  33253
  Copyright terms: Public domain W3C validator