Theorem 19.41v 1902

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 1526	. 2 |- ( ps -> A. x ps )
2	1	19.41h 1685	1 |- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.41vv  1903  19.41vvv  1904  19.41vvvv  1905  exdistrv  1910  eeeanv  1933  gencbvex  2785  euxfrdc  2925  euind  2926  dfdif3  3247  r19.9rmv  3516  opabm  4282  eliunxp  4768  relop  4779  dmuni  4839  dmres  4930  dminss  5045  imainss  5046  ssrnres  5073  cnvresima  5120  resco  5135  rnco  5137  coass  5149  xpcom  5177  f11o  5496  fvelrnb  5565  rnoprab  5960  domen  6753  xpassen  6832  genpassl  7525  genpassu  7526