Theorem r19.23v 2879

Description: Restricted quantifier version of 19.23v 1829. Version of r19.23 2878 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 298	. . 3 |- ( ( ph -> ps ) <-> ( -. ps -> -. ph ) )
2	1	ralbii 2831	. 2 |- ( A. x e. A ( ph -> ps ) <-> A. x e. A ( -. ps -> -. ph ) )
3		r19.21v 2805	. 2 |- ( A. x e. A ( -. ps -> -. ph ) <-> ( -. ps -> A. x e. A -. ph ) )
4		dfrex2 2850	. . . 4 |- ( E. x e. A ph <-> -. A. x e. A -. ph )
5	4	imbi1i 331	. . 3 |- ( ( E. x e. A ph -> ps ) <-> ( -. A. x e. A -. ph -> ps ) )
6		con1b 339	. . 3 |- ( ( -. A. x e. A -. ph -> ps ) <-> ( -. ps -> A. x e. A -. ph ) )
7	5, 6	bitr2i 258	. 2 |- ( ( -. ps -> A. x e. A -. ph ) <-> ( E. x e. A ph -> ps ) )
8	2, 3, 7	3bitri 279	1 |- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   A.wral 2749   E.wrex 2750

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

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-ral 2754  df-rex 2755

This theorem is referenced by:  rexlimiv  2885  ralxpxfr2d  3176  uniiunlem  3529  dfiin2g  4325  iunss  4333  ralxfr2d  4630  ssrel2  4944  reliun  4973  funimass4  5939  ralrnmpt2  6438  kmlem12  8617  fimaxre3  10581  gcdcllem1  14522  vdwmc2  14978  iunocv  19293  islindf4  19445  ovolgelb  22482  dyadmax  22605  itg2leub  22741  mptelee  24974  nmoubi  26462  nmopub  27610  nmfnleub  27627  sigaclcu2  28991  untuni  30385  dfpo2  30444  heibor1lem  32186  ispsubsp2  33356  pmapglbx  33379  2reu4a  38648