Theorem ralnex 2495

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 2490	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1627	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2491	. . 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 1516   e. wcel 2177   A.wral 2485   E.wrex 2486

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 1471  ax-gen 1473  ax-ie2 1518

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

This theorem is referenced by:  nnral  2497  rexalim  2500  ralinexa  2534  nrex  2599  nrexdv  2600  ralnex2  2646  r19.30dc  2654  uni0b  3884  iindif2m  4004  f0rn0  5487  supmoti  7116  fodjuomnilemdc  7267  ismkvnex  7278  nninfwlpoimlemginf  7299  suprnubex  9056  icc0r  10078  ioo0  10434  ico0  10436  ioc0  10437  prmind2  12527  sqrt2irr  12569  nconstwlpolem  16176