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

Theorem 19.41v 1838
Description: Version of 19.41 2070 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
19.41v  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem 19.41v
StepHypRef Expression
1 19.40 1739 . . 3  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  E. x ps ) )
2 19.9v 1820 . . . 4  |-  ( E. x ps  <->  ps )
32anbi2i 708 . . 3  |-  ( ( E. x ph  /\  E. x ps )  <->  ( E. x ph  /\  ps )
)
41, 3sylib 201 . 2  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  ps ) )
5 pm3.21 455 . . . 4  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
65eximdv 1772 . . 3  |-  ( ps 
->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) )
76impcom 437 . 2  |-  ( ( E. x ph  /\  ps )  ->  E. x
( ph  /\  ps )
)
84, 7impbii 192 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 376   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672
This theorem is referenced by:  19.41vv  1839  19.41vvv  1840  19.41vvvv  1841  19.42v  1842  equsexvw  1856  r19.41v  2928  gencbvex  3078  euxfr  3212  euind  3213  zfpair  4637  opabn0  4732  eliunxp  4977  relop  4990  dmuni  5050  dmres  5131  dminss  5256  imainss  5257  ssrnres  5281  cnvresima  5331  resco  5346  rnco  5348  coass  5361  xpco  5383  rnoprab  6398  f11o  6774  frxp  6925  omeu  7304  domen  7600  xpassen  7684  kmlem3  8600  cflem  8694  genpass  9452  ltexprlem4  9482  hasheqf1oi  12572  3v3e3cycl2  25471  bnj534  29620  bnj906  29813  bnj908  29814  bnj916  29816  bnj983  29834  bnj986  29837  dftr6  30461  bj-eeanvw  31373  bj-csbsnlem  31573  bj-ccinftydisj  31725  prter2  32517  dihglb2  34981  pm11.6  36812  pm11.71  36817  rfcnnnub  37420  eliunxp2  40623
  Copyright terms: Public domain W3C validator