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

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

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