Theorem ralnex 1656

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 1044	. 2 |- (A.x(x e. A -> -. ph) <-> -. E.x(x e. A /\ ph))
2		df-ral 1652	. 2 |- (A.x e. A -. ph <-> A.x(x e. A -> -. ph))
3		df-rex 1653	. . 3 |- (E.x e. A ph <-> E.x(x e. A /\ ph))
4	3	negbii 187	. 2 |- (-. E.x e. A ph <-> -. E.x(x e. A /\ ph))
5	1, 2, 4	3bitr4 183	1 |- (A.x e. A -. ph <-> -. E.x e. A ph)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 956   e. wcel 960  E.wex 982  A.wral 1648  E.wrex 1649

This theorem is referenced by:  dfrex2 1659  ralinexa 1686  nrex 1732  nrexdv 1733  ra4esbca 2002  iindif2 2616  ordunisuc2 3121  tfi 3132  rexxp 3225  canth 3913  omsdomnn 4538  isfinite2 4557  isfinite2OLD 4558  supmo 4585  elirrv 4607  unbndrank 4693  ac9s 4774  kmlem7 4781  kmlem8 4782  kmlem13 4787  zorn2lem4 4801  arch 6073  xrsupsslem 6078  xrinfmsslem 6079  supxrre 6085  supxrbnd 6093  supxrbnd1 6097  supxrbnd2 6098  sqr2irrlem3 6727  climunii 7098  clsval2 7682  ntreq0 7705  qdensere 7748  bcthlem7 8002  bcthlem28 8023  nmounbi 8435  lnon0 8454  hlimunii 9103  large 10189  cvbr2t 10205  chrelat2 10287

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-ral 1652  df-rex 1653

Copyright terms: Public domain