Theorem ralnex 2532

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 2527	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
2		alinexa 1652	. . 3 |- ( A. x ( x e. A -> -. ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2528	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 690	. 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 )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1396   E.wex 1541   e. wcel 2205   A.wral 2522   E.wrex 2523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ie2 1543

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-fal 1404  df-ral 2527  df-rex 2528

This theorem is referenced by:  nnral  2534  rexalim  2537  ralinexa  2571  nrex  2636  nrexdv  2637  ralnex2  2684  r19.30dc  2692  uni0b  3941  iindif2m  4061  f0rn0  5564  supmoti  7286  fodjuomnilemdc  7437  ismkvnex  7448  nninfwlpoimlemginf  7469  suprnubex  9229  icc0r  10262  ioo0  10623  ico0  10625  ioc0  10626  prmind2  12821  sqrt2irr  12863  umgrnloop0  16129  vtxd0nedgbfi  16311  1hevtxdg0fi  16319  nconstwlpolem  16868