Theorem rexanali 3102

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 3073	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2		iman 402	. . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
3	2	ralbii 3093	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
4	1, 3	xchbinxr 334	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wral 3061  ∃wrex 3070

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 206  df-an 397  df-ex 1782  df-ral 3062  df-rex 3071

This theorem is referenced by:  nrexralim  3137  ceqsralbv  3644  frpoind  6340  wfiOLD  6349  frind  9741  qsqueeze  13176  ncoprmgcdne1b  16583  elcls  22568  ist1-2  22842  haust1  22847  t1sep  22865  bwth  22905  1stccnp  22957  filufint  23415  fclscf  23520  pmltpc  24958  ovolgelb  24988  itg2seq  25251  radcnvlt1  25921  pntlem3  27101  nosupbnd1lem5  27204  noinfbnd1lem5  27219  umgr2edg1  28457  umgr2edgneu  28460  archiabl  32331  ordtconnlem1  32892  limsucncmpi  35318  matunitlindflem1  36472  ftc1anclem5  36553  clsk3nimkb  42776