Theorem ralnex 2521

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 2516	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1652	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2517	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 690	. 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 1396   E.wex 1541   e. wcel 2202   A.wral 2511   E.wrex 2512

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ie2 1543

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-fal 1404  df-ral 2516  df-rex 2517

This theorem is referenced by:  nnral  2523  rexalim  2526  ralinexa  2560  nrex  2625  nrexdv  2626  ralnex2  2673  r19.30dc  2681  uni0b  3923  iindif2m  4043  f0rn0  5540  supmoti  7252  fodjuomnilemdc  7403  ismkvnex  7414  nninfwlpoimlemginf  7435  suprnubex  9192  icc0r  10222  ioo0  10582  ico0  10584  ioc0  10585  prmind2  12772  sqrt2irr  12814  umgrnloop0  16058  vtxd0nedgbfi  16240  1hevtxdg0fi  16248  nconstwlpolem  16798