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  5590  supmoti  7339  fodjuomnilemdc  7490  ismkvnex  7501  nninfwlpoimlemginf  7522  suprnubex  9291  icc0r  10344  ioo0  10710  ico0  10712  ioc0  10713  prmind2  12922  sqrt2irr  12965  sqrtrirr  13013  umgrnloop0  16580  vtxd0nedgbfi  16762  1hevtxdg0fi  16770  nconstwlpolem  17339