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

Theorem 19.41 1799
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 1608 . . 3  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  E. x ps ) )
2 19.41.1 . . . . 5  |-  F/ x ps
3 id 21 . . . . 5  |-  ( ps 
->  ps )
42, 3exlimi 1781 . . . 4  |-  ( E. x ps  ->  ps )
54anim2i 555 . . 3  |-  ( ( E. x ph  /\  E. x ps )  -> 
( E. x ph  /\ 
ps ) )
61, 5syl 17 . 2  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  ps ) )
7 pm3.21 437 . . . 4  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
82, 7eximd 1711 . . 3  |-  ( ps 
->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) )
98impcom 421 . 2  |-  ( ( E. x ph  /\  ps )  ->  E. x
( ph  /\  ps )
)
106, 9impbii 182 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1537   F/wnf 1539
This theorem is referenced by:  19.42  1800  19.41v  2034  eean  2054  r19.41  2654  eliunxp  4730  dfopab2  6026  dfoprab3s  6027  xpcomco  6837  2sb5nd  27019  2sb5ndVD  27376  2sb5ndALT  27399  bnj605  27628  bnj607  27637
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator