Theorem rexanali 3094

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396  ∀wral 3054  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3055  df-rex 3065

This theorem is referenced by:  nrexralim  3124  ceqsralbv  3602  frpoind  6300  frind  9672  qsqueeze  13151  ncoprmgcdne1b  16617  elcls  23063  ist1-2  23337  haust1  23342  t1sep  23360  bwth  23400  1stccnp  23452  filufint  23910  fclscf  24015  pmltpc  25442  ovolgelb  25472  itg2seq  25734  radcnvlt1  26408  pntlem3  27597  nosupbnd1lem5  27701  noinfbnd1lem5  27716  oncutlt  28281  umgr2edg1  29305  umgr2edgneu  29308  archiabl  33286  extdgfialglem1  33883  ordtconnlem1  34115  limsucncmpi  36680  matunitlindflem1  37990  ftc1anclem5  38071  clsk3nimkb  44491