Theorem rexanali 3086

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 3059	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2		iman 401	. . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
3	2	ralbii 3078	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
4	1, 3	xchbinxr 335	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3047  ∃wrex 3056

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3048  df-rex 3057

This theorem is referenced by:  nrexralim  3116  ceqsralbv  3607  frpoind  6284  frind  9638  qsqueeze  13095  ncoprmgcdne1b  16556  elcls  22983  ist1-2  23257  haust1  23262  t1sep  23280  bwth  23320  1stccnp  23372  filufint  23830  fclscf  23935  pmltpc  25373  ovolgelb  25403  itg2seq  25665  radcnvlt1  26349  pntlem3  27542  nosupbnd1lem5  27646  noinfbnd1lem5  27661  onscutlt  28196  umgr2edg1  29184  umgr2edgneu  29187  archiabl  33159  extdgfialglem1  33697  ordtconnlem1  33929  limsucncmpi  36479  matunitlindflem1  37656  ftc1anclem5  37737  clsk3nimkb  44073