MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexanali Unicode version

Theorem rexanali 2589
Description: A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
Assertion
Ref Expression
rexanali  |-  ( E. x  e.  A  (
ph  /\  -.  ps )  <->  -. 
A. x  e.  A  ( ph  ->  ps )
)

Proof of Theorem rexanali
StepHypRef Expression
1 annim 414 . . 3  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
21rexbii 2568 . 2  |-  ( E. x  e.  A  (
ph  /\  -.  ps )  <->  E. x  e.  A  -.  ( ph  ->  ps )
)
3 rexnal 2554 . 2  |-  ( E. x  e.  A  -.  ( ph  ->  ps )  <->  -. 
A. x  e.  A  ( ph  ->  ps )
)
42, 3bitri 240 1  |-  ( E. x  e.  A  (
ph  /\  -.  ps )  <->  -. 
A. x  e.  A  ( ph  ->  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wral 2543   E.wrex 2544
This theorem is referenced by:  dfsup2OLD  7196  qsqueeze  10528  elcls  16810  ist1-2  17075  haust1  17080  t1sep  17098  1stccnp  17188  filufint  17615  fclscf  17720  pmltpc  18810  ovolgelb  18839  itg2seq  19097  radcnvlt1  19794  pntlem3  20758  wfi  24207  frind  24243  limsucncmpi  24884  negcmpprcal1  24945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator