Theorem alnex 1033

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

Syntax hints:  -. wn 2   <-> wb 146  A.wal 954  E.wex 980

This theorem is referenced by:  alex 1034  alinexa 1042  exanali 1043  alexn 1044  19.29 1071  19.43 1088  19.33b 1092  19.41 1095  nex 1101  nexd 1102  a12lem2 1377  mo 1393  mo2 1400  2mo 1447  mo2icl 1923  dm0rn0 3330  reldm0 3331  imadif 3574  fn0 3605  kmlem4 4768  axpowndlem3 4951  axpownd 4953  cnfilca 10583  cnfilcaOLD 10584

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 981

Copyright terms: Public domain