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

Theorem rexanali 2840
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 2838 . 2  |-  ( E. x  e.  A  (
ph  /\  -.  ps )  <->  -. 
A. x  e.  A  -.  ( ph  /\  -.  ps ) )
2 iman 426 . . 3  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
32ralbii 2819 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x  e.  A  -.  ( ph  /\  -.  ps )
)
41, 3xchbinxr 313 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 188    /\ wa 371   A.wral 2737   E.wrex 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-ral 2742  df-rex 2743
This theorem is referenced by:  nrexralim  2841  wfi  5413  qsqueeze  11494  ncoprmgcdne1b  14655  elcls  20089  ist1-2  20363  haust1  20368  t1sep  20386  bwth  20425  1stccnp  20477  filufint  20935  fclscf  21040  pmltpc  22401  ovolgelb  22433  itg2seq  22700  radcnvlt1  23373  pntlem3  24447  usgra2edg1  25110  archiabl  28515  ordtconlem1  28730  ceqsralv2  30358  frind  30481  limsucncmpi  31105  ftc1anclem5  32021  usgr2edg1  39292  usg2edgneu  39777
  Copyright terms: Public domain W3C validator