Theorem r19.23v 2823

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 1672	. 2 |- F/ x ps
2	1	r19.23 2822	1 |- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wral 2705   E.wrex 2706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711

This theorem is referenced by:  ralxpxfr2d  3073  uniiunlem  3428  dfiin2g  4191  iunss  4199  ralxfr2d  4496  ssrel2  4917  reliun  4947  funimass4  5730  ralrnmpt2  6194  kmlem12  8318  fimaxre3  10267  gcdcllem1  13678  vdwmc2  14023  iunocv  17948  islindf4  18109  ovolgelb  20805  dyadmax  20920  itg2leub  21054  mptelee  22964  nmoubi  23995  nmopub  25135  nmfnleub  25152  sigaclcu2  26417  untuni  27207  dfpo2  27412  heibor1lem  28552  2reu4a  29859  ispsubsp2  32984  pmapglbx  33007