Theorem rexnal 2114

Description: Relationship between restricted universal and existential quantifiers.

Assertion

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

Proof of Theorem rexnal

Step	Hyp	Ref	Expression
1		exanali 1390	. 2 |- (E.x(x e. A /\ -. ph) <-> -. A.x(x e. A -> ph))
2		df-rex 2110	. 2 |- (E.x e. A -. ph <-> E.x(x e. A /\ -. ph))
3		df-ral 2109	. . 3 |- (A.x e. A ph <-> A.x(x e. A -> ph))
4	3	notbii 204	. 2 |- (-. A.x e. A ph <-> -. A.x(x e. A -> ph))
5	1, 2, 4	3bitr4i 200	1 |- (E.x e. A -. ph <-> -. A.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:  dfral2 2115  rexanali 2144  2ralor 2250  uni0b 3203  iundif2 3322  elpwunsn 3856  ixp0 5420  isfinite2 5639  ordiso 5683  ordtypelem7 5690  unbndrank 5794  ac6n 5919  kmlem3 5929  kmlem7 5933  kmlem8 5934  kmlem13 5939  alephval2 6050  cfeq0 6062  arch 7280  xrsupsslem 7285  xrinfmsslem 7286  supxrbnd 7300  supxrbnd1 7304  supxrbnd2 7305  climunii 8358  climubii 8413  infxpidmlem8 8828  fctop 8920  cctop 8922  bcthlem33 9309  nmounbi 9778  hausfillim 10303  hlimuniii 10741  nmcopexlem1 11588  nmcfnexlem1 11617  bnj3 12368  alzdvds 13695  axdenselem4 14022  axdenselem5 14023  axfelem11 14041  axfelem15 14045  negcmpprcal2 14276  fordisxex 14291  dstr 14516  iintlem1 15010  lvsovso2 15039  supnuf 15041  supexr 15043  ordisoOLD 15374  ordtypelem7OLD 15381  reconnlem1 15446  reconnlem4 15449  isufil2 15565  ufileu 15573  fcluscf 15612  flimfnfcls 15615  2ralorOLD 15655  heiborlem23 15977  smprngpr 16200

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