Theorem 19.41v 1926

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.41vv  1927  19.41vvv  1928  19.41vvvv  1929  exdistrv  1934  eeeanv  1961  gencbvex  2819  euxfrdc  2959  euind  2960  dfdif3  3283  r19.9rmv  3552  opabm  4327  eliunxp  4817  relop  4828  dmuni  4888  dmres  4980  dminss  5097  imainss  5098  ssrnres  5125  cnvresima  5172  resco  5187  rnco  5189  coass  5201  xpcom  5229  f11o  5555  fvelrnb  5626  rnoprab  6028  domen  6840  xpassen  6925  genpassl  7637  genpassu  7638