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 402 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
32ralbii 3165 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
41, 3xchbinxr 336 1 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wral 3138  wrex 3139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-ral 3143  df-rex 3144
This theorem is referenced by:  nrexralim  3266  wfi  6175  qsqueeze  12584  ncoprmgcdne1b  15984  elcls  21611  ist1-2  21885  haust1  21890  t1sep  21908  bwth  21948  1stccnp  22000  filufint  22458  fclscf  22563  pmltpc  23980  ovolgelb  24010  itg2seq  24272  radcnvlt1  24935  pntlem3  26113  umgr2edg1  26921  umgr2edgneu  26924  archiabl  30755  ordtconnlem1  31067  ceqsralv2  32854  frpoind  32978  frind  32983  nosupbnd1lem5  33110  limsucncmpi  33691  matunitlindflem1  34770  ftc1anclem5  34853  clsk3nimkb  40270
  Copyright terms: Public domain W3C validator