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

Theorem rexanali 3192
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 3170 . 2 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2 iman 402 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
32ralbii 3092 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
41, 3xchbinxr 335 1 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wral 3064  wrex 3065
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 397  df-ex 1783  df-ral 3069  df-rex 3070
This theorem is referenced by:  nrexralim  3193  frpoind  6245  wfiOLD  6254  frind  9508  qsqueeze  12935  ncoprmgcdne1b  16355  elcls  22224  ist1-2  22498  haust1  22503  t1sep  22521  bwth  22561  1stccnp  22613  filufint  23071  fclscf  23176  pmltpc  24614  ovolgelb  24644  itg2seq  24907  radcnvlt1  25577  pntlem3  26757  umgr2edg1  27578  umgr2edgneu  27581  archiabl  31452  ordtconnlem1  31874  ceqsralv2  33670  nosupbnd1lem5  33915  noinfbnd1lem5  33930  limsucncmpi  34634  matunitlindflem1  35773  ftc1anclem5  35854  clsk3nimkb  41650
  Copyright terms: Public domain W3C validator