Theorem rexanali 3094

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395  ∀wral 3053  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-ral 3054  df-rex 3063

This theorem is referenced by:  nrexralim  3129  ceqsralbv  3637  frpoind  6333  wfiOLD  6342  frind  9741  qsqueeze  13177  ncoprmgcdne1b  16584  elcls  22899  ist1-2  23173  haust1  23178  t1sep  23196  bwth  23236  1stccnp  23288  filufint  23746  fclscf  23851  pmltpc  25301  ovolgelb  25331  itg2seq  25594  radcnvlt1  26271  pntlem3  27458  nosupbnd1lem5  27561  noinfbnd1lem5  27576  umgr2edg1  28937  umgr2edgneu  28940  archiabl  32812  ordtconnlem1  33393  limsucncmpi  35820  matunitlindflem1  36974  ftc1anclem5  37055  clsk3nimkb  43280