Theorem rexanali 3092

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 3052  ∃wrex 3061

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

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

This theorem is referenced by:  nrexralim  3125  ceqsralbv  3641  frpoind  6336  wfiOLD  6345  frind  9769  qsqueeze  13222  ncoprmgcdne1b  16674  elcls  23016  ist1-2  23290  haust1  23295  t1sep  23313  bwth  23353  1stccnp  23405  filufint  23863  fclscf  23968  pmltpc  25408  ovolgelb  25438  itg2seq  25700  radcnvlt1  26384  pntlem3  27577  nosupbnd1lem5  27681  noinfbnd1lem5  27696  onscutlt  28222  umgr2edg1  29195  umgr2edgneu  29198  archiabl  33201  ordtconnlem1  33960  limsucncmpi  36468  matunitlindflem1  37645  ftc1anclem5  37726  clsk3nimkb  44031