Theorem r19.23v 2943

Description: Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 31-Aug-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)

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		con34b 292	. . 3 |- ( ( ph -> ps ) <-> ( -. ps -> -. ph ) )
2	1	ralbii 2895	. 2 |- ( A. x e. A ( ph -> ps ) <-> A. x e. A ( -. ps -> -. ph ) )
3		r19.21v 2869	. 2 |- ( A. x e. A ( -. ps -> -. ph ) <-> ( -. ps -> A. x e. A -. ph ) )
4		dfrex2 2915	. . . 4 |- ( E. x e. A ph <-> -. A. x e. A -. ph )
5	4	imbi1i 325	. . 3 |- ( ( E. x e. A ph -> ps ) <-> ( -. A. x e. A -. ph -> ps ) )
6		con1b 333	. . 3 |- ( ( -. A. x e. A -. ph -> ps ) <-> ( -. ps -> A. x e. A -. ph ) )
7	5, 6	bitr2i 250	. 2 |- ( ( -. ps -> A. x e. A -. ph ) <-> ( E. x e. A ph -> ps ) )
8	2, 3, 7	3bitri 271	1 |- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   A.wral 2814   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820

This theorem is referenced by:  rexlimiv  2949  ralxpxfr2d  3228  uniiunlem  3588  dfiin2g  4358  iunss  4366  ralxfr2d  4663  ssrel2  5091  reliun  5121  funimass4  5916  ralrnmpt2  6399  kmlem12  8537  fimaxre3  10488  gcdcllem1  14001  vdwmc2  14349  iunocv  18476  islindf4  18637  ovolgelb  21623  dyadmax  21739  itg2leub  21873  mptelee  23871  nmoubi  25360  nmopub  26500  nmfnleub  26517  sigaclcu2  27757  untuni  28553  dfpo2  28758  heibor1lem  29906  2reu4a  31661  ispsubsp2  34542  pmapglbx  34565