Theorem r19.23v 2937

Description: Restricted quantifier version of 19.23v 1761. Version of r19.23 2936 with a dv condition. (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 2888	. 2 |- ( A. x e. A ( ph -> ps ) <-> A. x e. A ( -. ps -> -. ph ) )
3		r19.21v 2862	. 2 |- ( A. x e. A ( -. ps -> -. ph ) <-> ( -. ps -> A. x e. A -. ph ) )
4		dfrex2 2908	. . . 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 2807   E.wrex 2808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-ral 2812  df-rex 2813

This theorem is referenced by:  rexlimiv  2943  ralxpxfr2d  3224  uniiunlem  3584  dfiin2g  4365  iunss  4373  ralxfr2d  4672  ssrel2  5102  reliun  5132  funimass4  5924  ralrnmpt2  6416  kmlem12  8558  fimaxre3  10512  gcdcllem1  14160  vdwmc2  14508  iunocv  18838  islindf4  18999  ovolgelb  22016  dyadmax  22132  itg2leub  22266  mptelee  24324  nmoubi  25813  nmopub  26953  nmfnleub  26970  sigaclcu2  28281  untuni  29256  dfpo2  29359  heibor1lem  30467  2reu4a  32355  ispsubsp2  35571  pmapglbx  35594