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

Theorem 19.41v 1789
Description: Version of 19.41 1993 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 1694 . . 3  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  E. x ps ) )
2 19.9v 1772 . . . 4  |-  ( E. x ps  <->  ps )
32anbi2i 692 . . 3  |-  ( ( E. x ph  /\  E. x ps )  <->  ( E. x ph  /\  ps )
)
41, 3sylib 196 . 2  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  ps ) )
5 pm3.21 446 . . . 4  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
65eximdv 1725 . . 3  |-  ( ps 
->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) )
76impcom 428 . 2  |-  ( ( E. x ph  /\  ps )  ->  E. x
( ph  /\  ps )
)
84, 7impbii 188 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367   E.wex 1627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1628
This theorem is referenced by:  19.41vv  1790  19.41vvv  1791  19.41vvvv  1792  19.42v  1793  r19.41v  2951  gencbvex  3095  euxfr  3227  euind  3228  zfpair  4616  opabn0  4709  eliunxp  5070  relop  5083  dmuni  5142  dmres  5223  dminss  5347  imainss  5348  ssrnres  5372  cnvresima  5421  resco  5436  rnco  5438  coass  5451  xpco  5473  rnoprab  6306  f11o  6683  frxp  6831  omeu  7174  domen  7470  xpassen  7552  kmlem3  8467  cflem  8561  genpass  9320  ltexprlem4  9350  hasheqf1oi  12349  3v3e3cycl2  24810  dftr6  29385  prter2  30828  pm11.6  31506  pm11.71  31511  rfcnnnub  31618  eliunxp2  33162  bnj534  34181  bnj906  34374  bnj908  34375  bnj916  34377  bnj983  34395  bnj986  34398  bj-eeanvw  34653  bj-csbsnlem  34856  bj-ccinftydisj  35002  dihglb2  37521
  Copyright terms: Public domain W3C validator