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

Theorem alnex 1614
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 1613 . 2
21con2bii 332 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  A.wal 1393  E.wex 1612
This theorem is referenced by:  nex  1627  alex  1647  2exnaln  1650  aleximi  1653  eximOLD  1655  19.38  1662  alinexa  1663  alexn  1664  nexdh  1674  19.35OLD  1688  19.43  1693  19.43OLD  1694  19.33b  1696  nf4  1962  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  mo2OLD  2334  mo2icl  3278  disjsn  4090  dm0rn0  5224  reldm0  5225  iotanul  5571  imadif  5668  dffv2  5946  kmlem4  8554  axpowndlem3  8996  axpowndlem3OLD  8997  axpownd  8999  hashgt0elex  12466  nmo  27384  wl-nfeqfb  29990  wl-sb8et  30001  wl-lem-nexmo  30016  n0el  30600  pm10.251  31265  pm10.57  31276  elnev  31345  zrninitoringc  32879  alimp-no-surprise  33196  bnj1143  33849  bj-nf3  34197  bj-nexdh  34214  bj-hbntbi  34258
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 185  df-ex 1613
  Copyright terms: Public domain W3C validator