Theorem ralnex 1700

Description: Relationship between restricted universal and existential quantifiers.

Assertion

Ref	Expression
ralnex	|- (A.x e. A -. ph <-> -. E.x e. A ph)

Proof of Theorem ralnex

Step	Hyp	Ref	Expression
1		alinexa 1083	. 2 |- (A.x(x e. A -> -. ph) <-> -. E.x(x e. A /\ ph))
2		df-ral 1696	. 2 |- (A.x e. A -. ph <-> A.x(x e. A -> -. ph))
3		df-rex 1697	. . 3 |- (E.x e. A ph <-> E.x(x e. A /\ ph))
4	3	notbii 194	. 2 |- (-. E.x e. A ph <-> -. E.x(x e. A /\ ph))
5	1, 2, 4	3bitr4i 190	1 |- (A.x e. A -. ph <-> -. E.x e. A ph)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 153   /\ wa 230  A.wal 995   e. wcel 999  E.wex 1021  A.wral 1692  E.wrex 1693

This theorem is referenced by:  dfrex2 1703  ralinexa 1730  nrex 1776  nrexdv 1777  ra4esbca 2049  iindif2 2666  ordunisuc2 3172  tfi 3183  rexxp 3276  canth 3965  omsdomnn 4594  isfinite2 4609  supmo 4636  elirrv 4658  unbndrank 4745  ac9s 4826  kmlem7 4833  kmlem8 4834  kmlem13 4839  zorn2lem4 4853  arch 6153  xrsupsslem 6158  xrinfmsslem 6159  supxrre 6165  supxrbnd 6173  supxrbnd1 6177  supxrbnd2 6178  sqr2irrlem3 6816  climunii 7188  clsval2 7770  ntreq0 7793  qdensere 7836  bcthlem7 8090  bcthlem28 8111  nmounbi 8523  lnon0 8542  hlimuniii 9191  largei 10278  cvbr2 10294  chrelat2i 10376

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-ral 1696  df-rex 1697

Copyright terms: Public domain