Theorem alnex 1035

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 983	. 2 |- (E.xph <-> -. A.x -. ph)
2	1	con2bii 221	1 |- (A.x -. ph <-> -. E.xph)

Syntax hints:  -. wn 2   <-> wb 146  A.wal 956  E.wex 982

This theorem is referenced by:  alex 1036  alinexa 1044  exanali 1045  alexn 1046  19.29 1073  19.43 1090  19.33b 1094  19.41 1097  nex 1103  nexd 1104  a12lem2 1379  mo 1395  mo2 1402  2mo 1450  mo2icl 1926  dm0rn0 3336  reldm0 3337  imadif 3580  fn0 3611  kmlem4 4778  axpowndlem3 4963  axpownd 4965  cnfilca 10562

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 983

Copyright terms: Public domain