Theorem 19.41v 1914

Description: Version of 19.41 2103 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

Step	Hyp	Ref	Expression
1		19.40 1797	. . 3 |- ( E. x ( ph /\ ps ) -> ( E. x ph /\ E. x ps ) )
2		19.9v 1896	. . . 4 |- ( E. x ps <-> ps )
3	2	anbi2i 730	. . 3 |- ( ( E. x ph /\ E. x ps ) <-> ( E. x ph /\ ps ) )
4	1, 3	sylib 208	. 2 |- ( E. x ( ph /\ ps ) -> ( E. x ph /\ ps ) )
5		pm3.21 464	. . . 4 |- ( ps -> ( ph -> ( ph /\ ps ) ) )
6	5	eximdv 1846	. . 3 |- ( ps -> ( E. x ph -> E. x ( ph /\ ps ) ) )
7	6	impcom 446	. 2 |- ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) )
8	4, 7	impbii 199	1 |- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )

Syntax hints:   <-> wb 196   /\ wa 384   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  19.41vv  1915  19.41vvv  1916  19.41vvvv  1917  19.42v  1918  equsexvw  1932  r19.41v  3089  gencbvex  3250  euxfr  3392  euind  3393  zfpair  4904  opabn0  5006  eliunxp  5259  relop  5272  dmuni  5334  dmres  5419  dminss  5547  imainss  5548  ssrnres  5572  cnvresima  5623  resco  5639  rnco  5641  coass  5654  xpco  5675  rnoprab  6743  f11o  7128  frxp  7287  omeu  7665  domen  7968  xpassen  8054  kmlem3  8974  cflem  9068  genpass  9831  ltexprlem4  9861  hasheqf1oi  13140  hasheqf1oiOLD  13141  elwspths2spth  26862  bnj534  30808  bnj906  31000  bnj908  31001  bnj916  31003  bnj983  31021  bnj986  31024  dftr6  31640  bj-eeanvw  32704  bj-cleljustab  32847  bj-csbsnlem  32898  bj-rest10  33041  bj-restuni  33050  bj-ccinftydisj  33100  eldmqsres2  34052  prter2  34166  dihglb2  36631  pm11.6  38592  pm11.71  38597  rfcnnnub  39195  eliunxp2  42112