Theorem rexnal 2364

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 1679	. 2 |- (E.x(x e. A /\ -. ph) <-> -. A.x(x e. A -> ph))
2		df-rex 2360	. 2 |- (E.x e. A -. ph <-> E.x(x e. A /\ -. ph))
3		df-ral 2359	. . 3 |- (A.x e. A ph <-> A.x(x e. A -> ph))
4	3	notbii 300	. 2 |- (-. A.x e. A ph <-> -. A.x(x e. A -> ph))
5	1, 2, 4	3bitr4i 295	1 |- (E.x e. A -. ph <-> -. A.x e. A ph)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   /\ wa 337  A.wal 1584   e. wcel 1588  E.wex 1615  A.wral 2355  E.wrex 2356

This theorem is referenced by:  dfral2 2365  rexanali 2394  2ralor 2495  uni0b 3389  iundif2 3492  elpwunsn 4002  ixp0 5581  isfinite2 5858  ordiso 5914  ordtypelem7 5921  unbndrank 6030  infxpenlem 6147  cfeq0 6275  ac6n 6327  kmlem3 6339  kmlem7 6343  kmlem8 6344  kmlem13 6349  alephval2 6444  cfeq0OLD 6446  arch 7620  xrsupsslem 7625  xrinfmsslem 7626  supxrbnd 7640  supxrbnd1 7644  supxrbnd2 7645  climunii 8754  climubii 8809  infxpidmlem8OLD 9222  alzdvds 9288  fctop 9771  cctop 9773  bcthlem33 10175  nmounbi 10647  hausfillim 11141  hlimuniii 11575  nmcopexlem1 12420  nmcfnexlem1 12449  bnj3 13171  axdenselem4 14691  axdenselem5 14692  axfelem15 14713  axfelem18 14716  axfelem22 14720  elfuns 14774  negcmpprcal2 14976  fordisxex 14991  dstr 15255  iintlem1 15802  lvsovso2 15833  supnuf 15835  supexr 15837  ordisoOLD 16198  ordtypelem7OLD 16205  reconnlem1 16270  reconnlem4 16273  isufil2 16389  ufileu 16397  fcluscf 16436  flimfnfcls 16439  2ralorOLD 16479  heiborlem23 16801  smprngpr 17024

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1593  ax-4 1608  ax-5o 1610

This theorem depends on definitions:  df-bi 220  df-an 339  df-ex 1616  df-ral 2359  df-rex 2360

Copyright terms: Public domain