Theorem 19.41v 1830

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

Syntax hints:   /\ wa 102   <-> wb 103   E.wex 1426

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  19.41vv  1831  19.41vvv  1832  19.41vvvv  1833  eeeanv  1856  gencbvex  2665  euxfrdc  2801  euind  2802  dfdif3  3110  r19.9rmv  3373  opabm  4107  eliunxp  4575  relop  4586  dmuni  4646  dmres  4734  dminss  4846  imainss  4847  ssrnres  4873  cnvresima  4920  resco  4935  rnco  4937  coass  4949  xpcom  4977  f11o  5286  fvelrnb  5352  rnoprab  5731  domen  6466  xpassen  6544  genpassl  7081  genpassu  7082