Theorem rexanali 3116

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wral 3076  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3077  df-rex 3087

This theorem is used by:  nrexralim  3146  ceqsralbv  3610  frpoind  6345  frind  9758  qsqueeze  13335  ncoprmgcdne1b  16831  matunitlindflem1  23000  elcls  23397  ist1-2  23671  haust1  23676  t1sep  23694  bwth  23734  1stccnp  23787  filufint  24245  fclscf  24350  pmltpc  25777  ovolgelb  25807  itg2seq  26069  radcnvlt1  26751  pntlem3  27942  nosupbnd1lem5  28075  noinfbnd1lem5  28090  oncutlt  28656  umgr2edg1  29798  umgr2edgneu  29801  archiabl  33806  extdgfialglem1  34371  ordtconnlem1  34603  limsucncmpi  37326  ftc1anclem5  38709  clsk3nimkb  45134