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

Theorem 19.41v 1755
Description: Version of 19.41 1955 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 1664 . . 3  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  E. x ps ) )
2 19.9v 1739 . . . 4  |-  ( E. x ps  <->  ps )
32anbi2i 694 . . 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 448 . . . 4  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
65eximdv 1695 . . 3  |-  ( ps 
->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) )
76impcom 430 . 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 369   E.wex 1597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598
This theorem is referenced by:  19.41vv  1756  19.41vvv  1757  19.41vvvv  1758  19.42v  1759  gencbvex  3137  euxfr  3269  euind  3270  zfpair  4670  opabn0  4764  eliunxp  5126  relop  5139  dmuni  5198  dmres  5280  dminss  5406  imainss  5407  ssrnres  5431  cnvresima  5482  resco  5497  rnco  5499  coass  5512  xpco  5533  rnoprab  6366  f11o  6743  frxp  6891  omeu  7232  domen  7527  xpassen  7609  kmlem3  8530  cflem  8624  genpass  9385  ltexprlem4  9415  hasheqf1oi  12398  3v3e3cycl2  24529  dftr6  29147  prter2  30590  pm11.6  31245  pm11.71  31250  rfcnnnub  31358  eliunxp2  32631  bnj534  33503  bnj906  33695  bnj908  33696  bnj916  33698  bnj983  33716  bnj986  33719  bj-eeanvw  33981  bj-csbsnlem  34182  bj-ccinftydisj  34318  dihglb2  36771
  Copyright terms: Public domain W3C validator