Theorem 19.41v 1954

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  exdistrv  1962  eeeanv  1989  gencbvex  2863  euxfrdc  3005  euind  3006  dfdif3  3331  r19.9rmv  3603  opabm  4401  eliunxp  4896  relop  4907  dmuni  4968  dmres  5061  dminss  5179  imainss  5180  ssrnres  5207  cnvresima  5254  resco  5269  rnco  5271  coass  5283  xpcom  5311  f11o  5650  fvelrnb  5726  rnoprab  6138  domen  6990  xpassen  7083  genpassl  7841  genpassu  7842