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

Theorem 19.41 1979
Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1779 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 1687 . . 3  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  E. x ps ) )
2 19.41.1 . . . . 5  |-  F/ x ps
3219.9 1901 . . . 4  |-  ( E. x ps  <->  ps )
43anbi2i 692 . . 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 446 . . . 4  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
72, 6eximd 1890 . . 3  |-  ( ps 
->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) )
87impcom 428 . 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 367   E.wex 1620   F/wnf 1624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-12 1862
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-nf 1625
This theorem is referenced by:  19.42  1980  exan  1981  eean  1995  eeeanv  1997  2sb5rf  2199  r19.41  2935  eliunxp  5053  dfopab2  6753  dfoprab3s  6754  xpcomco  7526  mpt2mptxf  27665  eliunxp2  33123  2sb5nd  33673  2sb5ndVD  34057  2sb5ndALT  34079  bnj605  34312  bnj607  34321
  Copyright terms: Public domain W3C validator