Theorem ralnex 1653

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 1042	. 2 |- (A.x(x e. A -> -. ph) <-> -. E.x(x e. A /\ ph))
2		df-ral 1649	. 2 |- (A.x e. A -. ph <-> A.x(x e. A -> -. ph))
3		df-rex 1650	. . 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 954   e. wcel 958  E.wex 980  A.wral 1645  E.wrex 1646

This theorem is referenced by:  dfrex2 1656  ralinexa 1683  nrex 1729  nrexdv 1730  ra4esbca 1999  iindif2 2611  ordunisuc2 3115  tfi 3126  rexxp 3219  canth 3907  omsdomnn 4530  isfinite2OLD 4546  supmo 4576  elirrv 4598  unbndrank 4683  ac9s 4764  kmlem7 4771  kmlem8 4772  kmlem13 4777  zorn2lem4 4791  arch 6071  xrsupsslem 6076  xrinfmsslem 6077  supxrre 6083  supxrbnd 6091  supxrbnd1 6095  supxrbnd2 6096  sqr2irrlem3 6726  climunii 7098  clsval2 7685  ntreq0 7708  qdensere 7751  bcthlem7 8005  bcthlem28 8026  nmounbi 8439  lnon0 8458  hlimunii 9108  large 10194  cvbr2t 10210  chrelat2 10292

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-ral 1649  df-rex 1650

Copyright terms: Public domain