Theorem rexanali 2840

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 2838	. 2 |- ( E. x e. A ( ph /\ -. ps ) <-> -. A. x e. A -. ( ph /\ -. ps ) )
2		iman 426	. . 3 |- ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) )
3	2	ralbii 2819	. 2 |- ( A. x e. A ( ph -> ps ) <-> A. x e. A -. ( ph /\ -. ps ) )
4	1, 3	xchbinxr 313	1 |- ( E. x e. A ( ph /\ -. ps ) <-> -. A. x e. A ( ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   A.wral 2737   E.wrex 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-ral 2742  df-rex 2743

This theorem is referenced by:  nrexralim  2841  wfi  5413  qsqueeze  11494  ncoprmgcdne1b  14655  elcls  20089  ist1-2  20363  haust1  20368  t1sep  20386  bwth  20425  1stccnp  20477  filufint  20935  fclscf  21040  pmltpc  22401  ovolgelb  22433  itg2seq  22700  radcnvlt1  23373  pntlem3  24447  usgra2edg1  25110  archiabl  28515  ordtconlem1  28730  ceqsralv2  30358  frind  30481  limsucncmpi  31105  ftc1anclem5  32021  usgr2edg1  39292  usg2edgneu  39777