Theorem rexnal 2625

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 2620	. 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 2619	. . 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 2614  E.wrex 2615

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 2619  df-rex 2620

This theorem is referenced by:  dfral2  2626  rexanali  2660  2ralor  2780  uni0b  3916  iundif2  4033  dfint3  4318  dfnnc2  4395  nndisjeq  4429  ncfinraiselem2  4480  nnpweqlem1  4522  rexxpf  4828  transex  5910  refex  5911  antisymex  5912  connexex  5913  extex  5915  symex  5916  nchoicelem11  6299