Theorem rexanali 2917

Description: A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Proof shortened by Wolf Lammen, 27-Dec-2019.)

Assertion

Ref	Expression
rexanali	|- ( E. x e. A ( ph /\ -. ps ) <-> -. A. x e. A ( ph -> ps ) )

Proof of Theorem rexanali

Step	Hyp	Ref	Expression
1		dfrex2 2915	. 2 |- ( E. x e. A ( ph /\ -. ps ) <-> -. A. x e. A -. ( ph /\ -. ps ) )
2		iman 424	. . 3 |- ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) )
3	2	ralbii 2895	. 2 |- ( A. x e. A ( ph -> ps ) <-> A. x e. A -. ( ph /\ -. ps ) )
4	1, 3	xchbinxr 311	1 |- ( E. x e. A ( ph /\ -. ps ) <-> -. A. x e. A ( ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   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

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:  nrexralim  2918  dfsup2OLD  7903  qsqueeze  11400  elcls  19368  ist1-2  19642  haust1  19647  t1sep  19665  bwth  19704  1stccnp  19757  filufint  20184  fclscf  20289  pmltpc  21625  ovolgelb  21654  itg2seq  21912  radcnvlt1  22575  pntlem3  23550  usgra2edg1  24087  wfi  28892  frind  28928  limsucncmpi  29515  ftc1anclem5  29699  usg2edgneu  31907