Theorem alnex 1029

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

Syntax hints:  -. wn 2   <-> wb 146  A.wal 951  E.wex 977

This theorem is referenced by:  alex 1030  alinexa 1038  exanali 1039  alexn 1040  19.29 1067  19.43 1084  19.33b 1088  19.41 1091  nex 1097  nexd 1098  a12lem2 1370  mo 1386  mo2 1393  2mo 1440  mo2icl 1914  dm0rn0 3319  reldm0 3320  imadif 3560  fn0 3591  kmlem4 4740  axpowndlem3 4923  axpownd 4925  cnfilca 10451

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 978

Copyright terms: Public domain