Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fordisxex Unicode version

Theorem fordisxex 24954
Description: If  ( ph  \/  ps ) is true for all  x and  ps is not true for all  x then  ph is true for some  x. (Contributed by FL, 20-Apr-2011.)
Assertion
Ref Expression
fordisxex  |-  ( ( A. x  e.  A  ( ph  \/  ps )  /\  -.  A. x  e.  A  ps )  ->  E. x  e.  A  ph )

Proof of Theorem fordisxex
StepHypRef Expression
1 rexnal 2554 . 2  |-  ( E. x  e.  A  -.  ps 
<->  -.  A. x  e.  A  ps )
2 r19.29 2683 . . 3  |-  ( ( A. x  e.  A  ( ph  \/  ps )  /\  E. x  e.  A  -.  ps )  ->  E. x  e.  A  ( ( ph  \/  ps )  /\  -.  ps ) )
3 pm5.61 693 . . . . 5  |-  ( ( ( ph  \/  ps )  /\  -.  ps )  <->  (
ph  /\  -.  ps )
)
43simplbi 446 . . . 4  |-  ( ( ( ph  \/  ps )  /\  -.  ps )  ->  ph )
54reximi 2650 . . 3  |-  ( E. x  e.  A  ( ( ph  \/  ps )  /\  -.  ps )  ->  E. x  e.  A  ph )
62, 5syl 15 . 2  |-  ( ( A. x  e.  A  ( ph  \/  ps )  /\  E. x  e.  A  -.  ps )  ->  E. x  e.  A  ph )
71, 6sylan2br 462 1  |-  ( ( A. x  e.  A  ( ph  \/  ps )  /\  -.  A. x  e.  A  ps )  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357    /\ wa 358   A.wral 2543   E.wrex 2544
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-ex 1529  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator