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

Theorem rexanali 2753
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 416 . . 3  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
21rexbii 2732 . 2  |-  ( E. x  e.  A  (
ph  /\  -.  ps )  <->  E. x  e.  A  -.  ( ph  ->  ps )
)
3 rexnal 2718 . 2  |-  ( E. x  e.  A  -.  ( ph  ->  ps )  <->  -. 
A. x  e.  A  ( ph  ->  ps )
)
42, 3bitri 242 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 178    /\ wa 360   A.wral 2707   E.wrex 2708
This theorem is referenced by:  nrexralim  2754  dfsup2OLD  7451  qsqueeze  10792  elcls  17142  ist1-2  17416  haust1  17421  t1sep  17439  1stccnp  17530  filufint  17957  fclscf  18062  pmltpc  19352  ovolgelb  19381  itg2seq  19637  radcnvlt1  20339  pntlem3  21308  usgra2edg1  21408  wfi  25487  frind  25523  limsucncmpi  26200  ftc1anclem5  26298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-ral 2712  df-rex 2713
  Copyright terms: Public domain W3C validator