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

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

Proof of Theorem rexanali
StepHypRef Expression
1 dfrex2 2892 . 2  |-  ( E. x  e.  A  (
ph  /\  -.  ps )  <->  -. 
A. x  e.  A  -.  ( ph  /\  -.  ps ) )
2 iman 424 . . 3  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
32ralbii 2872 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x  e.  A  -.  ( ph  /\  -.  ps )
)
41, 3xchbinxr 311 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 2791   E.wrex 2792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-ral 2796  df-rex 2797
This theorem is referenced by:  nrexralim  2895  dfsup2OLD  7902  qsqueeze  11406  elcls  19444  ist1-2  19718  haust1  19723  t1sep  19741  bwth  19780  1stccnp  19833  filufint  20291  fclscf  20396  pmltpc  21732  ovolgelb  21761  itg2seq  22019  radcnvlt1  22682  pntlem3  23663  usgra2edg1  24252  archiabl  27612  ordtconlem1  27776  wfi  29259  frind  29295  limsucncmpi  29882  ftc1anclem5  30066  usg2edgneu  32250
  Copyright terms: Public domain W3C validator