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

Theorem r19.23v 2659
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 1605 . 2  |-  F/ x ps
21r19.23 2658 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wral 2543   E.wrex 2544
This theorem is referenced by:  uniiunlem  3260  dfiin2g  3936  iunss  3943  ralxfr2d  4550  reliun  4806  funimass4  5573  ralrnmpt2  5958  kmlem12  7787  fimaxre3  9703  gcdcllem1  12690  vdwmc2  13026  iunocv  16581  ovolgelb  18839  dyadmax  18953  itg2leub  19089  nmoubi  21350  nmopub  22488  nmfnleub  22505  esumcvg  23454  sigaclcu2  23481  untuni  24055  dfpo2  24112  mptelee  24523  heibor1lem  26533  ralxpxfr2d  26760  islindf4  27308  2reu4a  27967  ispsubsp2  29935  pmapglbx  29958
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator