Theorem rexanali 3117

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wral 3077  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3078  df-rex 3088

This theorem is used by:  nrexralim  3147  ceqsralbv  3611  frpoind  6344  frind  9747  qsqueeze  13324  ncoprmgcdne1b  16818  matunitlindflem1  22987  elcls  23384  ist1-2  23658  haust1  23663  t1sep  23681  bwth  23721  1stccnp  23774  filufint  24232  fclscf  24337  pmltpc  25764  ovolgelb  25794  itg2seq  26056  radcnvlt1  26738  pntlem3  27929  nosupbnd1lem5  28062  noinfbnd1lem5  28077  oncutlt  28643  umgr2edg1  29785  umgr2edgneu  29788  archiabl  33752  extdgfialglem1  34317  ordtconnlem1  34549  limsucncmpi  37213  ftc1anclem5  38595  clsk3nimkb  45025