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

Theorem rexanali 2759
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 425 . . 3  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
21rexbii 2738 . 2  |-  ( E. x  e.  A  (
ph  /\  -.  ps )  <->  E. x  e.  A  -.  ( ph  ->  ps )
)
3 rexnal 2724 . 2  |-  ( E. x  e.  A  -.  ( ph  ->  ps )  <->  -. 
A. x  e.  A  ( ph  ->  ps )
)
42, 3bitri 249 1  |-  ( E. x  e.  A  (
ph  /\  -.  ps )  <->  -. 
A. x  e.  A  ( ph  ->  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369   A.wral 2713   E.wrex 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-ral 2718  df-rex 2719
This theorem is referenced by:  nrexralim  2760  dfsup2OLD  7691  qsqueeze  11169  elcls  18675  ist1-2  18949  haust1  18954  t1sep  18972  bwth  19011  1stccnp  19064  filufint  19491  fclscf  19596  pmltpc  20932  ovolgelb  20961  itg2seq  21218  radcnvlt1  21881  pntlem3  22856  usgra2edg1  23300  wfi  27666  frind  27702  limsucncmpi  28289  ftc1anclem5  28468
  Copyright terms: Public domain W3C validator