Theorem ralnex 1645

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 1038	. 2 |- (A.x(x e. A -> -. ph) <-> -. E.x(x e. A /\ ph))
2		df-ral 1641	. 2 |- (A.x e. A -. ph <-> A.x(x e. A -> -. ph))
3		df-rex 1642	. . 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 951   e. wcel 955  E.wex 977  A.wral 1637  E.wrex 1638

This theorem is referenced by:  dfrex2 1648  ralinexa 1675  nrex 1721  nrexdv 1722  ra4esbca 1989  iindif2 2601  ordunisuc2 3105  tfi 3116  rexxp 3209  canth 3892  omsdomnn 4509  isfinite2 4523  supmo 4550  elirrv 4570  unbndrank 4655  ac9s 4736  kmlem7 4743  kmlem8 4744  kmlem13 4749  zorn2lem4 4763  arch 6018  xrsupsslem 6023  xrinfmsslem 6024  supxrre 6030  supxrbnd 6038  supxrbnd1 6042  supxrbnd2 6043  sqr2irrlem3 6656  climunii 7035  clsval2 7627  ntreq0 7650  qdensere 7691  bcthlem7 7939  bcthlem28 7960  nmounbi 8371  hlimunii 9029  large 10104  cvbr2t 10120  chrelat2 10200

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-ral 1641  df-rex 1642

Copyright terms: Public domain