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

Theorem rexanali 3265
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 3239 . 2 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2 iman 404 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
32ralbii 3165 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
41, 3xchbinxr 337 1 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wral 3138  wrex 3139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144
This theorem is referenced by:  nrexralim  3266  wfi  6176  qsqueeze  12588  ncoprmgcdne1b  15988  elcls  21675  ist1-2  21949  haust1  21954  t1sep  21972  bwth  22012  1stccnp  22064  filufint  22522  fclscf  22627  pmltpc  24045  ovolgelb  24075  itg2seq  24337  radcnvlt1  25000  pntlem3  26179  umgr2edg1  26987  umgr2edgneu  26990  archiabl  30822  ordtconnlem1  31162  ceqsralv2  32951  frpoind  33075  frind  33080  nosupbnd1lem5  33207  limsucncmpi  33788  matunitlindflem1  34882  ftc1anclem5  34965  clsk3nimkb  40383
  Copyright terms: Public domain W3C validator