Theorem ralnex 2398

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 2393	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1563	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2394	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 655	. 2 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x e. A ph )
5	1, 4	bitri 183	1 |- ( A. x e. A -. ph <-> -. E. x e. A ph )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1310   E.wex 1449   e. wcel 1461   A.wral 2388   E.wrex 2389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-5 1404  ax-gen 1406  ax-ie2 1451

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-fal 1318  df-ral 2393  df-rex 2394

This theorem is referenced by:  rexalim  2402  ralinexa  2434  nrex  2496  nrexdv  2497  ralnex2  2543  uni0b  3725  iindif2m  3844  f0rn0  5273  supmoti  6830  fodjuomnilemdc  6964  suprnubex  8615  icc0r  9596  ioo0  9924  ico0  9926  ioc0  9927  prmind2  11641  sqrt2irr  11680