Theorem rexanali 3119

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 3092	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2		iman 406	. . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
3	2	ralbii 3111	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
4	1, 3	xchbinxr 338	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wral 3079  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is referenced by:  nrexralim  3149  ceqsralbv  3617  frpoind  6345  frind  9723  qsqueeze  13228  ncoprmgcdne1b  16709  elcls  23211  ist1-2  23485  haust1  23490  t1sep  23508  bwth  23548  1stccnp  23600  filufint  24058  fclscf  24163  pmltpc  25590  ovolgelb  25620  itg2seq  25882  radcnvlt1  26562  pntlem3  27754  nosupbnd1lem5  27857  noinfbnd1lem5  27872  oncutlt  28438  umgr2edg1  29542  umgr2edgneu  29545  archiabl  33499  extdgfialglem1  34063  ordtconnlem1  34295  limsucncmpi  36937  matunitlindflem1  38248  ftc1anclem5  38329  clsk3nimkb  44749