Theorem rexanali 3087

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	⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

Proof of Theorem rexanali

Step	Hyp	Ref	Expression
1		dfrex2 3060	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2		iman 401	. . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
3	2	ralbii 3079	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
4	1, 3	xchbinxr 335	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3048  ∃wrex 3057

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3049  df-rex 3058

This theorem is referenced by:  nrexralim  3117  ceqsralbv  3608  frpoind  6297  frind  9654  qsqueeze  13107  ncoprmgcdne1b  16568  elcls  23008  ist1-2  23282  haust1  23287  t1sep  23305  bwth  23345  1stccnp  23397  filufint  23855  fclscf  23960  pmltpc  25398  ovolgelb  25428  itg2seq  25690  radcnvlt1  26374  pntlem3  27567  nosupbnd1lem5  27671  noinfbnd1lem5  27686  onscutlt  28221  umgr2edg1  29210  umgr2edgneu  29213  archiabl  33208  extdgfialglem1  33777  ordtconnlem1  34009  limsucncmpi  36561  matunitlindflem1  37729  ftc1anclem5  37810  clsk3nimkb  44197