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  7192  fodjuomnilemdc  7343  ismkvnex  7354  nninfwlpoimlemginf  7375  suprnubex  9133  icc0r  10161  ioo0  10520  ico0  10522  ioc0  10523  prmind2  12710  sqrt2irr  12752  umgrnloop0  15987  vtxd0nedgbfi  16169  1hevtxdg0fi  16177  nconstwlpolem  16721