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 )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1400   E.wex 1545   e. wcel 2209   A.wral 2528   E.wrex 2529

This proof depends on 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 proof depends on definitions:  df-bi 117  df-tru 1405  df-fal 1408  df-ral 2533  df-rex 2534

This theorem is used by:  nnral  2540  rexalim  2543  ralinexa  2577  nrex  2642  nrexdv  2643  ralnex2  2690  r19.30dc  2698  uni0b  3960  iindif2m  4080  f0rn0  5587  supmoti  7333  fodjuomnilemdc  7484  ismkvnex  7495  nninfwlpoimlemginf  7516  suprnubex  9283  icc0r  10328  ioo0  10694  ico0  10696  ioc0  10697  prmind2  12898  sqrt2irr  12940  umgrnloop0  16358  vtxd0nedgbfi  16540  1hevtxdg0fi  16548  nconstwlpolem  17115