Theorem 19.41v 1875

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

Syntax hints:   /\ wa 103   <-> wb 104   E.wex 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.41vv  1876  19.41vvv  1877  19.41vvvv  1878  exdistrv  1883  eeeanv  1906  gencbvex  2735  euxfrdc  2874  euind  2875  dfdif3  3191  r19.9rmv  3459  opabm  4210  eliunxp  4686  relop  4697  dmuni  4757  dmres  4848  dminss  4961  imainss  4962  ssrnres  4989  cnvresima  5036  resco  5051  rnco  5053  coass  5065  xpcom  5093  f11o  5408  fvelrnb  5477  rnoprab  5862  domen  6653  xpassen  6732  genpassl  7356  genpassu  7357