Theorem rexnal 2626

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)

Assertion

Ref	Expression
rexnal	|- (E.x e. A -. ph <-> -. A.x e. A ph)

Proof of Theorem rexnal

Step	Hyp	Ref	Expression
1		df-rex 2621	. 2 |- (E.x e. A -. ph <-> E.x(x e. A /\ -. ph))
2		exanali 1585	. . 3 |- (E.x(x e. A /\ -. ph) <-> -. A.x(x e. A -> ph))
3		df-ral 2620	. . 3 |- (A.x e. A ph <-> A.x(x e. A -> ph))
4	2, 3	xchbinxr 302	. 2 |- (E.x(x e. A /\ -. ph) <-> -. A.x e. A ph)
5	1, 4	bitri 240	1 |- (E.x e. A -. ph <-> -. A.x e. A ph)

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540  E.wex 1541   e. wcel 1710  A.wral 2615  E.wrex 2616

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-an 360  df-ex 1542  df-ral 2620  df-rex 2621

This theorem is referenced by:  dfral2  2627  rexanali  2661  2ralor  2781  uni0b  3917  iundif2  4034  dfint3  4319  dfnnc2  4396  nndisjeq  4430  ncfinraiselem2  4481  nnpweqlem1  4523  rexxpf  4829  transex  5911  refex  5912  antisymex  5913  connexex  5914  extex  5916  symex  5917  nchoicelem11  6300