Theorem ralnex 2482

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 2477	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1614	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2478	. . 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 1503   e. wcel 2164   A.wral 2472   E.wrex 2473

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 1458  ax-gen 1460  ax-ie2 1505

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

This theorem is referenced by:  nnral  2484  rexalim  2487  ralinexa  2521  nrex  2586  nrexdv  2587  ralnex2  2633  r19.30dc  2641  uni0b  3861  iindif2m  3981  f0rn0  5449  supmoti  7054  fodjuomnilemdc  7205  ismkvnex  7216  nninfwlpoimlemginf  7237  suprnubex  8974  icc0r  9995  ioo0  10331  ico0  10333  ioc0  10334  prmind2  12261  sqrt2irr  12303  nconstwlpolem  15625