Theorem ralnex 2458

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 2453	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1596	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2454	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 678	. 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 1346   E.wex 1485   e. wcel 2141   A.wral 2448   E.wrex 2449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-ie2 1487

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-fal 1354  df-ral 2453  df-rex 2454

This theorem is referenced by:  nnral  2460  rexalim  2463  ralinexa  2497  nrex  2562  nrexdv  2563  ralnex2  2609  r19.30dc  2617  uni0b  3821  iindif2m  3940  f0rn0  5392  supmoti  6970  fodjuomnilemdc  7120  ismkvnex  7131  nninfwlpoimlemginf  7152  suprnubex  8869  icc0r  9883  ioo0  10216  ico0  10218  ioc0  10219  prmind2  12074  sqrt2irr  12116  nconstwlpolem  14096