Theorem rexanali 3121

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

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

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3082  df-rex 3092

This theorem is used by:  nrexralim  3151  ceqsralbv  3618  frpoind  6347  frind  9725  qsqueeze  13238  ncoprmgcdne1b  16725  elcls  23259  ist1-2  23533  haust1  23538  t1sep  23556  bwth  23596  1stccnp  23648  filufint  24106  fclscf  24211  pmltpc  25638  ovolgelb  25668  itg2seq  25930  radcnvlt1  26610  pntlem3  27802  nosupbnd1lem5  27905  noinfbnd1lem5  27920  oncutlt  28486  umgr2edg1  29590  umgr2edgneu  29593  archiabl  33541  extdgfialglem1  34105  ordtconnlem1  34337  limsucncmpi  36989  matunitlindflem1  38300  ftc1anclem5  38381  clsk3nimkb  44799