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

Theorem alnex 1783
 Description: Universal quantification of negation is equivalent to negation of existential quantification. Dual of exnal 1828 (but does not depend on ax-4 1811 contrary to it). See also the dual pair df-ex 1782 / alex 1827. 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 1782 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
21con2bii 361 1 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1536  ∃wex 1781 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 210  df-ex 1782 This theorem is referenced by:  nf3  1788  nfntht2  1796  nex  1802  alex  1827  2exnaln  1830  aleximi  1833  19.38  1840  alinexa  1844  alexn  1846  nexdh  1867  19.43  1884  19.43OLD  1885  19.33b  1887  empty  1908  cbvexdvaw  2047  cbvexdw  2361  cbvex  2419  cbvexvOLD  2423  cbvexd  2431  dfmoeu  2620  nexmo  2625  euae  2748  ralnex  3230  cbvrexdva2OLD  3443  vtoclgft  3539  mo2icl  3691  n0el  4304  falseral0  4442  disjsn  4632  axprlem5  5315  dm0rn0  5782  reldm0  5785  iotanul  6321  imadif  6426  dffv2  6747  kmlem4  9577  axpowndlem3  10019  axpownd  10021  hashgt0elex  13767  nelbOLD  30241  nmo  30263  bnj1143  32119  unbdqndv1  33904  bj-nexdh  34018  axc11n11r  34074  bj-hbntbi  34095  bj-modal4e  34106  wl-nfeqfb  34886  wl-sb8et  34899  wl-lem-nexmo  34913  wl-dfrexsb  34961  pm10.251  40984  pm10.57  40995  elnev  41062  spr0nelg  43919  zrninitoringc  44621  alimp-no-surprise  45235
 Copyright terms: Public domain W3C validator