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

Theorem rexanali 3106
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 3077 . 2 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2 iman 403 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
32ralbii 3097 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
41, 3xchbinxr 335 1 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wral 3065  wrex 3074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3066  df-rex 3075
This theorem is referenced by:  nrexralim  3135  ceqsralbv  3608  frpoind  6297  wfiOLD  6306  frind  9687  qsqueeze  13121  ncoprmgcdne1b  16527  elcls  22427  ist1-2  22701  haust1  22706  t1sep  22724  bwth  22764  1stccnp  22816  filufint  23274  fclscf  23379  pmltpc  24817  ovolgelb  24847  itg2seq  25110  radcnvlt1  25780  pntlem3  26960  nosupbnd1lem5  27063  noinfbnd1lem5  27078  umgr2edg1  28162  umgr2edgneu  28165  archiabl  32037  ordtconnlem1  32508  limsucncmpi  34920  matunitlindflem1  36077  ftc1anclem5  36158  clsk3nimkb  42319
  Copyright terms: Public domain W3C validator