Theorem ralnex 2485

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 2480	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1617	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2481	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 684	. 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 1362   E.wex 1506   e. wcel 2167   A.wral 2475   E.wrex 2476

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 615  ax-in2 616  ax-5 1461  ax-gen 1463  ax-ie2 1508

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-fal 1370  df-ral 2480  df-rex 2481

This theorem is referenced by:  nnral  2487  rexalim  2490  ralinexa  2524  nrex  2589  nrexdv  2590  ralnex2  2636  r19.30dc  2644  uni0b  3864  iindif2m  3984  f0rn0  5452  supmoti  7059  fodjuomnilemdc  7210  ismkvnex  7221  nninfwlpoimlemginf  7242  suprnubex  8980  icc0r  10001  ioo0  10349  ico0  10351  ioc0  10352  prmind2  12288  sqrt2irr  12330  nconstwlpolem  15709