Theorem r19.23v 2905

Description: Restricted quantifier version of 19.23v 1807. Version of r19.23 2904 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 293	. . 3 |- ( ( ph -> ps ) <-> ( -. ps -> -. ph ) )
2	1	ralbii 2856	. 2 |- ( A. x e. A ( ph -> ps ) <-> A. x e. A ( -. ps -> -. ph ) )
3		r19.21v 2830	. 2 |- ( A. x e. A ( -. ps -> -. ph ) <-> ( -. ps -> A. x e. A -. ph ) )
4		dfrex2 2876	. . . 4 |- ( E. x e. A ph <-> -. A. x e. A -. ph )
5	4	imbi1i 326	. . 3 |- ( ( E. x e. A ph -> ps ) <-> ( -. A. x e. A -. ph -> ps ) )
6		con1b 334	. . 3 |- ( ( -. A. x e. A -. ph -> ps ) <-> ( -. ps -> A. x e. A -. ph ) )
7	5, 6	bitr2i 253	. 2 |- ( ( -. ps -> A. x e. A -. ph ) <-> ( E. x e. A ph -> ps ) )
8	2, 3, 7	3bitri 274	1 |- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   A.wral 2775   E.wrex 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2780  df-rex 2781

This theorem is referenced by:  rexlimiv  2911  ralxpxfr2d  3196  uniiunlem  3549  dfiin2g  4329  iunss  4337  ralxfr2d  4633  ssrel2  4940  reliun  4969  funimass4  5928  ralrnmpt2  6421  kmlem12  8591  fimaxre3  10553  gcdcllem1  14460  vdwmc2  14916  iunocv  19230  islindf4  19382  ovolgelb  22419  dyadmax  22542  itg2leub  22678  mptelee  24911  nmoubi  26398  nmopub  27546  nmfnleub  27563  sigaclcu2  28937  untuni  30331  dfpo2  30389  heibor1lem  32054  ispsubsp2  33229  pmapglbx  33252  2reu4a  38322