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

Theorem 19.41 1815
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 1596 . . 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 1801 . . . 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 1750 . . 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 1528   F/wnf 1531
This theorem is referenced by:  19.42  1816  19.41v  1842  eean  1853  r19.41  2692  eliunxp  4823  dfopab2  6174  dfoprab3s  6175  xpcomco  6952  2sb5nd  28326  2sb5ndVD  28686  2sb5ndALT  28709  bnj605  28939  bnj607  28948
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator