Theorem rexanali 3115

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 3088	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2		iman 405	. . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
3	2	ralbii 3107	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
4	1, 3	xchbinxr 337	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  ∀wral 3075  ∃wrex 3085

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-ral 3076  df-rex 3086

This theorem is referenced by:  nrexralim  3145  ceqsralbv  3615  frpoind  6324  frind  9702  qsqueeze  13198  ncoprmgcdne1b  16675  elcls  23121  ist1-2  23395  haust1  23400  t1sep  23418  bwth  23458  1stccnp  23510  filufint  23968  fclscf  24073  pmltpc  25500  ovolgelb  25530  itg2seq  25792  radcnvlt1  26469  pntlem3  27661  nosupbnd1lem5  27764  noinfbnd1lem5  27779  oncutlt  28345  umgr2edg1  29369  umgr2edgneu  29372  archiabl  33339  extdgfialglem1  33950  ordtconnlem1  34182  limsucncmpi  36766  matunitlindflem1  38076  ftc1anclem5  38157  clsk3nimkb  44577