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

Theorem 19.41 1827
Description: Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
19.41.1  |-  F/ x ps
Assertion
Ref Expression
19.41  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )

Proof of Theorem 19.41
StepHypRef Expression
1 19.40 1599 . . 3  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  E. x ps ) )
2 19.41.1 . . . . 5  |-  F/ x ps
3 id 19 . . . . 5  |-  ( ps 
->  ps )
42, 3exlimi 1813 . . . 4  |-  ( E. x ps  ->  ps )
54anim2i 552 . . 3  |-  ( ( E. x ph  /\  E. x ps )  -> 
( E. x ph  /\ 
ps ) )
61, 5syl 15 . 2  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  ps ) )
7 pm3.21 435 . . . 4  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
82, 7eximd 1762 . . 3  |-  ( ps 
->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) )
98impcom 419 . 2  |-  ( ( E. x ph  /\  ps )  ->  E. x
( ph  /\  ps )
)
106, 9impbii 180 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1531   F/wnf 1534
This theorem is referenced by:  19.42  1828  19.41v  1854  eean  1865  r19.41  2705  eliunxp  4839  dfopab2  6190  dfoprab3s  6191  xpcomco  6968  2sb5nd  28625  2sb5ndVD  29002  2sb5ndALT  29025  bnj605  29255  bnj607  29264  eeanOLD7  29656
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator