Theorem 19.41v 1823

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

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

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  19.41vv  1824  19.41vvv  1825  19.41vvvv  1826  eeeanv  1849  gencbvex  2645  euxfrdc  2778  euind  2779  r19.9rmv  3333  opabm  4035  eliunxp  4493  relop  4504  dmuni  4563  dmres  4650  dminss  4758  imainss  4759  ssrnres  4783  cnvresima  4830  resco  4845  rnco  4847  coass  4859  xpcom  4884  f11o  5179  fvelrnb  5242  rnoprab  5607  domen  6255  xpassen  6327  genpassl  6714  genpassu  6715