Theorem rexanali 3136

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 3134	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2		iman 439	. . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
3	2	ralbii 3118	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
4	1, 3	xchbinxr 324	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383  ∀wral 3050  ∃wrex 3051

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

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-ral 3055  df-rex 3056

This theorem is referenced by:  nrexralim  3137  wfi  5874  qsqueeze  12245  ncoprmgcdne1b  15585  elcls  21099  ist1-2  21373  haust1  21378  t1sep  21396  bwth  21435  1stccnp  21487  filufint  21945  fclscf  22050  pmltpc  23439  ovolgelb  23468  itg2seq  23728  radcnvlt1  24391  pntlem3  25518  umgr2edg1  26323  umgr2edgneu  26326  archiabl  30082  ordtconnlem1  30300  ceqsralv2  31935  frpoind  32067  frind  32070  nosupbnd1lem5  32185  limsucncmpi  32771  matunitlindflem1  33736  ftc1anclem5  33820  clsk3nimkb  38858