Theorem rexanali 3175

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 3152	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2		iman 405	. . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
3	2	ralbii 3080	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
4	1, 3	xchbinxr 338	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wral 3053  ∃wrex 3054

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-ral 3058  df-rex 3059

This theorem is referenced by:  nrexralim  3176  wfi  6162  qsqueeze  12677  ncoprmgcdne1b  16091  elcls  21824  ist1-2  22098  haust1  22103  t1sep  22121  bwth  22161  1stccnp  22213  filufint  22671  fclscf  22776  pmltpc  24202  ovolgelb  24232  itg2seq  24495  radcnvlt1  25165  pntlem3  26345  umgr2edg1  27153  umgr2edgneu  27156  archiabl  31029  ordtconnlem1  31446  ceqsralv2  33243  frpoind  33383  frind  33391  nosupbnd1lem5  33556  noinfbnd1lem5  33571  limsucncmpi  34272  matunitlindflem1  35396  ftc1anclem5  35477  clsk3nimkb  41196