Theorem ralnex 2426

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 2421	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1582	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2422	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 672	. 2 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x e. A ph )
5	1, 4	bitri 183	1 |- ( A. x e. A -. ph <-> -. E. x e. A ph )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1329   E.wex 1468   e. wcel 1480   A.wral 2416   E.wrex 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-5 1423  ax-gen 1425  ax-ie2 1470

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-fal 1337  df-ral 2421  df-rex 2422

This theorem is referenced by:  rexalim  2430  ralinexa  2462  nrex  2524  nrexdv  2525  ralnex2  2571  uni0b  3761  iindif2m  3880  f0rn0  5317  supmoti  6880  fodjuomnilemdc  7016  ismkvnex  7029  suprnubex  8711  icc0r  9709  ioo0  10037  ico0  10039  ioc0  10040  prmind2  11801  sqrt2irr  11840