Theorem ralnex 2454

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 2449	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1591	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2450	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 673	. 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 1341   E.wex 1480   e. wcel 2136   A.wral 2444   E.wrex 2445

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 604  ax-in2 605  ax-5 1435  ax-gen 1437  ax-ie2 1482

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-fal 1349  df-ral 2449  df-rex 2450

This theorem is referenced by:  nnral  2456  rexalim  2459  ralinexa  2493  nrex  2558  nrexdv  2559  ralnex2  2605  r19.30dc  2613  uni0b  3814  iindif2m  3933  f0rn0  5382  supmoti  6958  fodjuomnilemdc  7108  ismkvnex  7119  suprnubex  8848  icc0r  9862  ioo0  10195  ico0  10197  ioc0  10198  prmind2  12052  sqrt2irr  12094  nconstwlpolem  13943