Theorem ralnex 2538

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 2533	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1656	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2534	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 694	. 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 1400   E.wex 1545   e. wcel 2209   A.wral 2528   E.wrex 2529

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 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ie2 1547

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-fal 1408  df-ral 2533  df-rex 2534

This theorem is referenced by:  nnral  2540  rexalim  2543  ralinexa  2577  nrex  2642  nrexdv  2643  ralnex2  2690  r19.30dc  2698  uni0b  3958  iindif2m  4078  f0rn0  5585  supmoti  7326  fodjuomnilemdc  7477  ismkvnex  7488  nninfwlpoimlemginf  7509  suprnubex  9276  icc0r  10310  ioo0  10675  ico0  10677  ioc0  10678  prmind2  12879  sqrt2irr  12921  umgrnloop0  16275  vtxd0nedgbfi  16457  1hevtxdg0fi  16465  nconstwlpolem  17023