Theorem ralnex 2520

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

Assertion

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

Proof of Theorem ralnex

Step	Hyp	Ref	Expression
1		df-ral 2515	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1651	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2516	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 689	. 2 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x e. A ph )
5	1, 4	bitri 184	1 |- ( A. x e. A -. ph <-> -. E. x e. A ph )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1395   E.wex 1540   e. wcel 2202   A.wral 2510   E.wrex 2511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-5 1495  ax-gen 1497  ax-ie2 1542

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-fal 1403  df-ral 2515  df-rex 2516

This theorem is referenced by:  nnral  2522  rexalim  2525  ralinexa  2559  nrex  2624  nrexdv  2625  ralnex2  2672  r19.30dc  2680  uni0b  3918  iindif2m  4038  f0rn0  5531  supmoti  7191  fodjuomnilemdc  7342  ismkvnex  7353  nninfwlpoimlemginf  7374  suprnubex  9132  icc0r  10160  ioo0  10518  ico0  10520  ioc0  10521  prmind2  12691  sqrt2irr  12733  umgrnloop0  15967  vtxd0nedgbfi  16149  1hevtxdg0fi  16157  nconstwlpolem  16669