Theorem 19.41v 1917

Description: Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-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		ax-17 1540	. 2 |- ( ps -> A. x ps )
2	1	19.41h 1699	1 |- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )

Syntax hints:   /\ wa 104   <-> wb 105   E.wex 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.41vv  1918  19.41vvv  1919  19.41vvvv  1920  exdistrv  1925  eeeanv  1952  gencbvex  2810  euxfrdc  2950  euind  2951  dfdif3  3273  r19.9rmv  3542  opabm  4315  eliunxp  4805  relop  4816  dmuni  4876  dmres  4967  dminss  5084  imainss  5085  ssrnres  5112  cnvresima  5159  resco  5174  rnco  5176  coass  5188  xpcom  5216  f11o  5537  fvelrnb  5608  rnoprab  6005  domen  6810  xpassen  6889  genpassl  7591  genpassu  7592