Theorem alnex 1039

Description: Theorem 19.7 of [Margaris] p. 89.

Assertion

Ref	Expression
alnex	|- (A.x -. ph <-> -. E.xph)

Proof of Theorem alnex

Step	Hyp	Ref	Expression
1		df-ex 985	. 2 |- (E.xph <-> -. A.x -. ph)
2	1	con2bii 221	1 |- (A.x -. ph <-> -. E.xph)

Syntax hints:  -. wn 2   <-> wb 146  A.wal 958  E.wex 984

This theorem is referenced by:  alex 1040  alinexa 1048  exanali 1049  alexn 1050  19.29 1077  19.43 1094  19.33b 1098  19.41 1101  nex 1107  nexd 1108  a12lem2 1383  mo 1399  mo2 1406  2mo 1454  mo2icl 1930  dm0rn0 3344  reldm0 3345  imadif 3588  fn0 3619  kmlem4 4780  axpowndlem3 4964  axpownd 4966  cnfilca 10582

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-ex 985

Copyright terms: Public domain