Theorem 19.41v 1927

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.41vv  1928  19.41vvv  1929  19.41vvvv  1930  exdistrv  1935  eeeanv  1962  gencbvex  2824  euxfrdc  2966  euind  2967  dfdif3  3291  r19.9rmv  3560  opabm  4345  eliunxp  4835  relop  4846  dmuni  4907  dmres  4999  dminss  5116  imainss  5117  ssrnres  5144  cnvresima  5191  resco  5206  rnco  5208  coass  5220  xpcom  5248  f11o  5577  fvelrnb  5649  rnoprab  6051  domen  6863  xpassen  6950  genpassl  7672  genpassu  7673