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

Theorem alnex 1696
Description: Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)
Assertion
Ref Expression
alnex (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Proof of Theorem alnex
StepHypRef Expression
1 df-ex 1695 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
21con2bii 345 1 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wal 1472  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  nex  1709  alex  1731  2exnaln  1734  aleximi  1737  19.38  1745  alinexa  1747  alexn  1748  nexdh  1760  19.43  1780  19.43OLD  1781  19.33b  1783  nexdv  1817  nf4  2092  cbvexdva  2174  mo2v  2369  ralnex  2879  mo2icl  3256  disjsn  4095  dm0rn0  5154  reldm0  5155  iotanul  5668  imadif  5772  dffv2  6064  kmlem4  8733  axpowndlem3  9175  axpownd  9177  hashgt0elex  12913  nmo  28498  bnj1143  29961  unbdqndv1  31504  bj-nf3  31602  bj-nexdh  31625  bj-modal5e  31660  axc11n11r  31695  bj-hbntbi  31717  bj-modal4e  31727  wl-nf4  32298  wl-nfnt  32312  wl-nfeqfb  32377  wl-sb8et  32388  wl-lem-nexmo  32403  n0el  33039  pm10.251  37463  pm10.57  37474  elnev  37543  falseral0  40203  zrninitoringc  41955  alimp-no-surprise  42389
  Copyright terms: Public domain W3C validator