Theorem r19.23v 3023

Description: Restricted quantifier version of 19.23v 1902. Version of r19.23 3022 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 306	. . 3 |- ( ( ph -> ps ) <-> ( -. ps -> -. ph ) )
2	1	ralbii 2980	. 2 |- ( A. x e. A ( ph -> ps ) <-> A. x e. A ( -. ps -> -. ph ) )
3		r19.21v 2960	. 2 |- ( A. x e. A ( -. ps -> -. ph ) <-> ( -. ps -> A. x e. A -. ph ) )
4		dfrex2 2996	. . . 4 |- ( E. x e. A ph <-> -. A. x e. A -. ph )
5	4	imbi1i 339	. . 3 |- ( ( E. x e. A ph -> ps ) <-> ( -. A. x e. A -. ph -> ps ) )
6		con1b 348	. . 3 |- ( ( -. A. x e. A -. ph -> ps ) <-> ( -. ps -> A. x e. A -. ph ) )
7	5, 6	bitr2i 265	. 2 |- ( ( -. ps -> A. x e. A -. ph ) <-> ( E. x e. A ph -> ps ) )
8	2, 3, 7	3bitri 286	1 |- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   A.wral 2912   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  rexlimiv  3027  ralxpxfr2d  3327  uniiunlem  3691  dfiin2g  4553  iunss  4561  ralxfr2d  4882  ssrel2  5210  reliun  5239  funimass4  6247  ralrnmpt2  6775  kmlem12  8983  fimaxre3  10970  gcdcllem1  15221  vdwmc2  15683  iunocv  20025  islindf4  20177  ovolgelb  23248  dyadmax  23366  itg2leub  23501  mptelee  25775  nmoubi  27627  nmopub  28767  nmfnleub  28784  sigaclcu2  30183  untuni  31586  dfpo2  31645  elintfv  31662  heibor1lem  33608  ispsubsp2  35032  pmapglbx  35055  neik0pk1imk0  38345  2reu4a  41189