Theorem ralnex 2518

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 2513	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1649	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2514	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 687	. 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 1393   E.wex 1538   e. wcel 2200   A.wral 2508   E.wrex 2509

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ie2 1540

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-fal 1401  df-ral 2513  df-rex 2514

This theorem is referenced by:  nnral  2520  rexalim  2523  ralinexa  2557  nrex  2622  nrexdv  2623  ralnex2  2670  r19.30dc  2678  uni0b  3913  iindif2m  4033  f0rn0  5520  supmoti  7160  fodjuomnilemdc  7311  ismkvnex  7322  nninfwlpoimlemginf  7343  suprnubex  9100  icc0r  10122  ioo0  10479  ico0  10481  ioc0  10482  prmind2  12642  sqrt2irr  12684  umgrnloop0  15917  nconstwlpolem  16433