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

Theorem 19.41 2062
Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1841 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)
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 1742 . . 3  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  E. x ps ) )
2 19.41.1 . . . . 5  |-  F/ x ps
3219.9 1981 . . . 4  |-  ( E. x ps  <->  ps )
43anbi2i 705 . . 3  |-  ( ( E. x ph  /\  E. x ps )  <->  ( E. x ph  /\  ps )
)
51, 4sylib 201 . 2  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  ps ) )
6 pm3.21 454 . . . 4  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
72, 6eximd 1971 . . 3  |-  ( ps 
->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) )
87impcom 436 . 2  |-  ( ( E. x ph  /\  ps )  ->  E. x
( ph  /\  ps )
)
95, 8impbii 192 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375   E.wex 1674   F/wnf 1678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679
This theorem is referenced by:  19.42  2063  exan  2064  equsexv  2077  eean  2088  eeeanv  2090  equsexALT  2142  2sb5rf  2291  r19.41  2955  eliunxp  4991  dfopab2  6874  dfoprab3s  6875  xpcomco  7688  mpt2mptxf  28329  bnj605  29767  bnj607  29776  2sb5nd  36971  2sb5ndVD  37347  2sb5ndALT  37369  eliunxp2  40388
  Copyright terms: Public domain W3C validator