NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  alnex GIF version

Theorem alnex 1543
Description: Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
alnex (x ¬ φ ↔ ¬ xφ)

Proof of Theorem alnex
StepHypRef Expression
1 df-ex 1542 . 2 (xφ ↔ ¬ x ¬ φ)
21con2bii 322 1 (x ¬ φ ↔ ¬ xφ)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 176  wal 1540  wex 1541
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ex 1542
This theorem is referenced by:  nex  1555  alex  1572  exim  1575  alinexa  1578  alexn  1579  nexdh  1589  19.35  1600  19.43  1605  19.43OLD  1606  19.33b  1608  19.38  1794  nf4  1868  mo  2226  mo2  2233  2mo  2282  axi11e  2332  mo2icl  3015  disjsn  3786  dfimak2  4298  iotanul  4354  dm0rn0  4921  dmeq0  4922  imadif  5171
  Copyright terms: Public domain W3C validator