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  10345  ioo0  10711  ico0  10713  ioc0  10714  prmind2  12923  sqrt2irr  12966  sqrtrirr  13014  umgrnloop0  16563  vtxd0nedgbfi  16745  1hevtxdg0fi  16753  nconstwlpolem  17322