Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexanali Structured version   Visualization version   GIF version

Theorem rexanali 3027
 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
StepHypRef Expression
1 dfrex2 3025 . 2 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2 iman 439 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
32ralbii 3009 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
41, 3xchbinxr 324 1 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383  ∀wral 2941  ∃wrex 2942 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947 This theorem is referenced by:  nrexralim  3028  wfi  5751  qsqueeze  12070  ncoprmgcdne1b  15410  elcls  20925  ist1-2  21199  haust1  21204  t1sep  21222  bwth  21261  1stccnp  21313  filufint  21771  fclscf  21876  pmltpc  23265  ovolgelb  23294  itg2seq  23554  radcnvlt1  24217  pntlem3  25343  umgr2edg1  26148  umgr2edgneu  26151  archiabl  29880  ordtconnlem1  30098  ceqsralv2  31733  frpoind  31865  frind  31868  nosupbnd1lem5  31983  limsucncmpi  32569  matunitlindflem1  33535  ftc1anclem5  33619  clsk3nimkb  38655
 Copyright terms: Public domain W3C validator