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

Theorem rexanali 3136
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 3134 . 2 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
2 iman 439 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
32ralbii 3118 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴 ¬ (𝜑 ∧ ¬ 𝜓))
41, 3xchbinxr 324 1 (∃𝑥𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  wral 3050  wrex 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-ral 3055  df-rex 3056
This theorem is referenced by:  nrexralim  3137  wfi  5874  qsqueeze  12245  ncoprmgcdne1b  15585  elcls  21099  ist1-2  21373  haust1  21378  t1sep  21396  bwth  21435  1stccnp  21487  filufint  21945  fclscf  22050  pmltpc  23439  ovolgelb  23468  itg2seq  23728  radcnvlt1  24391  pntlem3  25518  umgr2edg1  26323  umgr2edgneu  26326  archiabl  30082  ordtconnlem1  30300  ceqsralv2  31935  frpoind  32067  frind  32070  nosupbnd1lem5  32185  limsucncmpi  32771  matunitlindflem1  33736  ftc1anclem5  33820  clsk3nimkb  38858
  Copyright terms: Public domain W3C validator