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

Theorem 19.41 1957
Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1757 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 1666 . . 3  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  E. x ps ) )
2 19.41.1 . . . . 5  |-  F/ x ps
3219.9 1879 . . . 4  |-  ( E. x ps  <->  ps )
43anbi2i 694 . . 3  |-  ( ( E. x ph  /\  E. x ps )  <->  ( E. x ph  /\  ps )
)
51, 4sylib 196 . 2  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  ps ) )
6 pm3.21 448 . . . 4  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
72, 6eximd 1868 . . 3  |-  ( ps 
->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) )
87impcom 430 . 2  |-  ( ( E. x ph  /\  ps )  ->  E. x
( ph  /\  ps )
)
95, 8impbii 188 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1599   F/wnf 1603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-nf 1604
This theorem is referenced by:  19.42  1958  exan  1959  eean  1973  eeeanv  1975  2sb5rf  2181  r19.41  2996  eliunxp  5130  dfopab2  6839  dfoprab3s  6840  xpcomco  7609  mpt2mptxf  27496  eliunxp2  32791  2sb5nd  33201  2sb5ndVD  33578  2sb5ndALT  33600  bnj605  33833  bnj607  33842
  Copyright terms: Public domain W3C validator