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  5587  supmoti  7334  fodjuomnilemdc  7485  ismkvnex  7496  nninfwlpoimlemginf  7517  suprnubex  9286  icc0r  10339  ioo0  10705  ico0  10707  ioc0  10708  prmind2  12917  sqrt2irr  12960  sqrtrirr  13008  umgrnloop0  16524  vtxd0nedgbfi  16706  1hevtxdg0fi  16714  nconstwlpolem  17282