Theorem rexanali 3091

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 3064	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2		iman 401	. . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
3	2	ralbii 3083	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
4	1, 3	xchbinxr 335	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3052  df-rex 3062

This theorem is referenced by:  nrexralim  3121  ceqsralbv  3599  frpoind  6306  frind  9674  qsqueeze  13153  ncoprmgcdne1b  16619  elcls  23038  ist1-2  23312  haust1  23317  t1sep  23335  bwth  23375  1stccnp  23427  filufint  23885  fclscf  23990  pmltpc  25417  ovolgelb  25447  itg2seq  25709  radcnvlt1  26383  pntlem3  27572  nosupbnd1lem5  27676  noinfbnd1lem5  27691  oncutlt  28256  umgr2edg1  29280  umgr2edgneu  29283  archiabl  33259  extdgfialglem1  33836  ordtconnlem1  34068  limsucncmpi  36627  matunitlindflem1  37937  ftc1anclem5  38018  clsk3nimkb  44467