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

Theorem rexanali 2720
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 415 . . 3  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
21rexbii 2699 . 2  |-  ( E. x  e.  A  (
ph  /\  -.  ps )  <->  E. x  e.  A  -.  ( ph  ->  ps )
)
3 rexnal 2685 . 2  |-  ( E. x  e.  A  -.  ( ph  ->  ps )  <->  -. 
A. x  e.  A  ( ph  ->  ps )
)
42, 3bitri 241 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 177    /\ wa 359   A.wral 2674   E.wrex 2675
This theorem is referenced by:  dfsup2OLD  7414  qsqueeze  10751  elcls  17100  ist1-2  17373  haust1  17378  t1sep  17396  1stccnp  17486  filufint  17913  fclscf  18018  pmltpc  19308  ovolgelb  19337  itg2seq  19595  radcnvlt1  20295  pntlem3  21264  usgra2edg1  21364  wfi  25429  frind  25465  limsucncmpi  26107
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-ral 2679  df-rex 2680
  Copyright terms: Public domain W3C validator