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

Theorem rexanali 3175
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 3152 . 2 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2 iman 405 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
32ralbii 3080 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
41, 3xchbinxr 338 1 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wral 3053  wrex 3054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-ral 3058  df-rex 3059
This theorem is referenced by:  nrexralim  3176  wfi  6162  qsqueeze  12677  ncoprmgcdne1b  16091  elcls  21824  ist1-2  22098  haust1  22103  t1sep  22121  bwth  22161  1stccnp  22213  filufint  22671  fclscf  22776  pmltpc  24202  ovolgelb  24232  itg2seq  24495  radcnvlt1  25165  pntlem3  26345  umgr2edg1  27153  umgr2edgneu  27156  archiabl  31029  ordtconnlem1  31446  ceqsralv2  33243  frpoind  33383  frind  33391  nosupbnd1lem5  33556  noinfbnd1lem5  33571  limsucncmpi  34272  matunitlindflem1  35396  ftc1anclem5  35477  clsk3nimkb  41196
  Copyright terms: Public domain W3C validator