Theorem rexanali 3100

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394  ∀wral 3059  ∃wrex 3068

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 206  df-an 395  df-ex 1780  df-ral 3060  df-rex 3069

This theorem is referenced by:  nrexralim  3135  ceqsralbv  3644  frpoind  6342  wfiOLD  6351  frind  9747  qsqueeze  13184  ncoprmgcdne1b  16591  elcls  22797  ist1-2  23071  haust1  23076  t1sep  23094  bwth  23134  1stccnp  23186  filufint  23644  fclscf  23749  pmltpc  25199  ovolgelb  25229  itg2seq  25492  radcnvlt1  26166  pntlem3  27348  nosupbnd1lem5  27451  noinfbnd1lem5  27466  umgr2edg1  28735  umgr2edgneu  28738  archiabl  32614  ordtconnlem1  33202  limsucncmpi  35633  matunitlindflem1  36787  ftc1anclem5  36868  clsk3nimkb  43093