Theorem 19.41v 1914

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.41vv  1915  19.41vvv  1916  19.41vvvv  1917  exdistrv  1922  eeeanv  1949  gencbvex  2807  euxfrdc  2947  euind  2948  dfdif3  3270  r19.9rmv  3539  opabm  4312  eliunxp  4802  relop  4813  dmuni  4873  dmres  4964  dminss  5081  imainss  5082  ssrnres  5109  cnvresima  5156  resco  5171  rnco  5173  coass  5185  xpcom  5213  f11o  5534  fvelrnb  5605  rnoprab  6002  domen  6807  xpassen  6886  genpassl  7586  genpassu  7587