Theorem exnal 1574

Description: Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem exnal

Step	Hyp	Ref	Expression
1		alex 1572	. 2 |- (A.xph <-> -. E.x -. ph)
2	1	con2bii 322	1 |- (E.x -. ph <-> -. A.xph)

Syntax hints:  -. wn 3   <-> wb 176  A.wal 1540  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  alexn  1579  exanali  1585  19.30  1604  excom  1741  ax12olem5  1931  ax10lem2  1937  equsex  1962  spc3gv  2944  necompl  3544  opkelimagekg  4271  dfpw2  4327  dfaddc2  4381  nnsucelrlem1  4424  eqpw1relk  4479  eqtfinrelk  4486  setconslem2  4732  setconslem3  4733  setconslem7  4737  dfswap2  4741  nfunv  5138  brimage  5793  releqel  5807  releqmpt2  5809  ovcelem1  6171  tcfnex  6244  nchoicelem10  6298  fnfreclem1  6317