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

Theorem 19.41 1817
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 1597 . . 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 1803 . . . 4  |-  ( E. x ps  ->  ps )
54anim2i 554 . . 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 1752 . . 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 1529   F/wnf 1532
This theorem is referenced by:  19.42  1818  19.41v  1844  eean  1855  r19.41  2694  eliunxp  4823  dfopab2  6136  dfoprab3s  6137  xpcomco  6948  2sb5nd  27598  2sb5ndVD  27955  2sb5ndALT  27978  bnj605  28207  bnj607  28216
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-nf 1533
  Copyright terms: Public domain W3C validator