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

Step	Hyp	Ref	Expression
1		nfv 1674	. 2 |- F/ x ps
2	1	r19.23 2936	1 |- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )

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