Theorem ralnex 2113

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 1389	. 2 |- (A.x(x e. A -> -. ph) <-> -. E.x(x e. A /\ ph))
2		df-ral 2109	. 2 |- (A.x e. A -. ph <-> A.x(x e. A -> -. ph))
3		df-rex 2110	. . 3 |- (E.x e. A ph <-> E.x(x e. A /\ ph))
4	3	notbii 204	. 2 |- (-. E.x e. A ph <-> -. E.x(x e. A /\ ph))
5	1, 2, 4	3bitr4i 200	1 |- (A.x e. A -. ph <-> -. E.x e. A ph)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106

This theorem is referenced by:  dfrex2 2116  ralinexa 2143  nrex 2192  nrexdv 2193  rexim 2194  r19.43 2238  ra4esbca 2538  iindif2 3324  ordunisuc2 3926  tfi 3937  rexxp 4042  rexxpf 4044  canth 5112  omsdomnn 5623  isfinite2 5639  supmo 5666  ordiso 5683  ordtypelem4 5687  ordtypelem7 5690  elirrv 5700  unbndrank 5794  infenomsub 5889  ac9s 5926  kmlem7 5933  kmlem8 5934  kmlem13 5939  zorn2lem4 5953  arch 7280  xrsupsslem 7285  xrinfmsslem 7286  supxrre 7292  supxrbnd 7300  supxrbnd1 7304  supxrbnd2 7305  sqr2irrlem3 7976  climunii 8358  clsval2 8961  ntreq0 8984  qdensere 9027  bcthlem7 9283  bcthlem28 9304  nmounbi 9778  lnon0 9798  filrn 10293  hausfillim 10303  hlimuniii 10741  largei 11839  cvbr2 11855  chrelat2i 11937  bnj51 12426  dfon2lem8 13856  negcmpprcal1 14275  negcmpprcal2 14276  dstr 14516  lvsovso2 15039  ordisoOLD 15374  ordtypelem4OLD 15378  ordtypelem7OLD 15381  infenomsubOLD 15398  compfipin0 15436  alexsublem3 15439  alexsublem4 15440  rabeq0 15666  0nelqs2 16269  cvrnbtwn 16990  cvrval2 16991  hlrelat2 17052

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-ral 2109  df-rex 2110

Copyright terms: Public domain