Theorem rexanali 2759

Description: A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)

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		annim 425	. . 3 |- ( ( ph /\ -. ps ) <-> -. ( ph -> ps ) )
2	1	rexbii 2738	. 2 |- ( E. x e. A ( ph /\ -. ps ) <-> E. x e. A -. ( ph -> ps ) )
3		rexnal 2724	. 2 |- ( E. x e. A -. ( ph -> ps ) <-> -. A. x e. A ( ph -> ps ) )
4	2, 3	bitri 249	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 2713   E.wrex 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-ral 2718  df-rex 2719

This theorem is referenced by:  nrexralim  2760  dfsup2OLD  7691  qsqueeze  11169  elcls  18675  ist1-2  18949  haust1  18954  t1sep  18972  bwth  19011  1stccnp  19064  filufint  19491  fclscf  19596  pmltpc  20932  ovolgelb  20961  itg2seq  21218  radcnvlt1  21881  pntlem3  22856  usgra2edg1  23300  wfi  27666  frind  27702  limsucncmpi  28289  ftc1anclem5  28468