Theorem ralnex 2494

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 2489	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1626	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2490	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 685	. 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 1371   E.wex 1515   e. wcel 2176   A.wral 2484   E.wrex 2485

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 1470  ax-gen 1472  ax-ie2 1517

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-fal 1379  df-ral 2489  df-rex 2490

This theorem is referenced by:  nnral  2496  rexalim  2499  ralinexa  2533  nrex  2598  nrexdv  2599  ralnex2  2645  r19.30dc  2653  uni0b  3875  iindif2m  3995  f0rn0  5472  supmoti  7097  fodjuomnilemdc  7248  ismkvnex  7259  nninfwlpoimlemginf  7280  suprnubex  9028  icc0r  10050  ioo0  10404  ico0  10406  ioc0  10407  prmind2  12475  sqrt2irr  12517  nconstwlpolem  16041