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

Theorem rexanali 2917
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 2915 . 2  |-  ( E. x  e.  A  (
ph  /\  -.  ps )  <->  -. 
A. x  e.  A  -.  ( ph  /\  -.  ps ) )
2 iman 424 . . 3  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
32ralbii 2895 . 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 2814   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  nrexralim  2918  dfsup2OLD  7903  qsqueeze  11400  elcls  19368  ist1-2  19642  haust1  19647  t1sep  19665  bwth  19704  1stccnp  19757  filufint  20184  fclscf  20289  pmltpc  21625  ovolgelb  21654  itg2seq  21912  radcnvlt1  22575  pntlem3  23550  usgra2edg1  24087  wfi  28892  frind  28928  limsucncmpi  29515  ftc1anclem5  29699  usg2edgneu  31907
  Copyright terms: Public domain W3C validator