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  3274  r19.9rmv  3543  opabm  4316  eliunxp  4806  relop  4817  dmuni  4877  dmres  4968  dminss  5085  imainss  5086  ssrnres  5113  cnvresima  5160  resco  5175  rnco  5177  coass  5189  xpcom  5217  f11o  5540  fvelrnb  5611  rnoprab  6009  domen  6819  xpassen  6898  genpassl  7608  genpassu  7609