Theorem rexanali 3263

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 3237	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2		iman 404	. . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
3	2	ralbii 3163	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
4	1, 3	xchbinxr 337	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wral 3136  ∃wrex 3137

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-ral 3141  df-rex 3142

This theorem is referenced by:  nrexralim  3264  wfi  6174  qsqueeze  12586  ncoprmgcdne1b  15986  elcls  21673  ist1-2  21947  haust1  21952  t1sep  21970  bwth  22010  1stccnp  22062  filufint  22520  fclscf  22625  pmltpc  24043  ovolgelb  24073  itg2seq  24335  radcnvlt1  24998  pntlem3  26177  umgr2edg1  26985  umgr2edgneu  26988  archiabl  30820  ordtconnlem1  31160  ceqsralv2  32949  frpoind  33073  frind  33078  nosupbnd1lem5  33205  limsucncmpi  33786  matunitlindflem1  34880  ftc1anclem5  34963  clsk3nimkb  40380