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  3860  iindif2m  3980  f0rn0  5448  supmoti  7052  fodjuomnilemdc  7203  ismkvnex  7214  nninfwlpoimlemginf  7235  suprnubex  8972  icc0r  9992  ioo0  10328  ico0  10330  ioc0  10331  prmind2  12258  sqrt2irr  12300  nconstwlpolem  15555