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

Theorem rexanali 3102
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 3073 . 2 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2 iman 401 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
32ralbii 3093 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
41, 3xchbinxr 335 1 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wral 3061  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062  df-rex 3071
This theorem is referenced by:  nrexralim  3137  ceqsralbv  3657  frpoind  6363  wfiOLD  6372  frind  9790  qsqueeze  13243  ncoprmgcdne1b  16687  elcls  23081  ist1-2  23355  haust1  23360  t1sep  23378  bwth  23418  1stccnp  23470  filufint  23928  fclscf  24033  pmltpc  25485  ovolgelb  25515  itg2seq  25777  radcnvlt1  26461  pntlem3  27653  nosupbnd1lem5  27757  noinfbnd1lem5  27772  umgr2edg1  29228  umgr2edgneu  29231  archiabl  33205  ordtconnlem1  33923  limsucncmpi  36446  matunitlindflem1  37623  ftc1anclem5  37704  clsk3nimkb  44053
  Copyright terms: Public domain W3C validator