Theorem rexnal 1654

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 1043	. 2 |- (E.x(x e. A /\ -. ph) <-> -. A.x(x e. A -> ph))
2		df-rex 1650	. 2 |- (E.x e. A -. ph <-> E.x(x e. A /\ -. ph))
3		df-ral 1649	. . 3 |- (A.x e. A ph <-> A.x(x e. A -> ph))
4	3	negbii 187	. 2 |- (-. A.x e. A ph <-> -. A.x(x e. A -> ph))
5	1, 2, 4	3bitr4 183	1 |- (E.x e. A -. ph <-> -. A.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:  dfral2 1655  rexanali 1684  uni0b 2523  iundif2 2610  elpwunsn 2912  ixp0 4361  isfinite2OLD 4546  unbndrank 4683  ac6n 4757  kmlem3 4767  kmlem7 4771  kmlem8 4772  kmlem13 4777  alephval2 4902  cfeq0 4914  arch 6071  xrsupsslem 6076  xrinfmsslem 6077  supxrbnd 6091  supxrbnd1 6095  supxrbnd2 6096  climunii 7098  climubi 7153  infxpidmlem8 7559  fctopOLD 7650  cctop 7652  bcthlem33 8031  nmounbi 8439  hlimunii 9108  nmcopexlem1 9951  nmcfnexlem1 9980  iintlem1 10632

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