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

Theorem rexanali 2878
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 2876 . 2  |-  ( E. x  e.  A  (
ph  /\  -.  ps )  <->  -. 
A. x  e.  A  -.  ( ph  /\  -.  ps ) )
2 iman 425 . . 3  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
32ralbii 2856 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x  e.  A  -.  ( ph  /\  -.  ps )
)
41, 3xchbinxr 312 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 187    /\ wa 370   A.wral 2775   E.wrex 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2780  df-rex 2781
This theorem is referenced by:  nrexralim  2879  wfi  5428  qsqueeze  11494  ncoprmgcdne1b  14640  elcls  20073  ist1-2  20347  haust1  20352  t1sep  20370  bwth  20409  1stccnp  20461  filufint  20919  fclscf  21024  pmltpc  22385  ovolgelb  22417  itg2seq  22684  radcnvlt1  23357  pntlem3  24431  usgra2edg1  25094  archiabl  28507  ordtconlem1  28723  frind  30473  limsucncmpi  31095  ftc1anclem5  31932  usg2edgneu  38910
  Copyright terms: Public domain W3C validator