Theorem rexlimivw 2590

Description: Weaker version of rexlimiv 2588. (Contributed by FL, 19-Sep-2011.)

Hypothesis

Ref	Expression
rexlimivw.1	|- ( ph -> ps )

Assertion

Ref	Expression
rexlimivw	|- ( E. x e. A ph -> ps )

Distinct variable group:   ps, x

Allowed substitution hints:   ph( x)   A( x)

Proof of Theorem rexlimivw

Step	Hyp	Ref	Expression
1		rexlimivw.1	. . 3 |- ( ph -> ps )
2	1	a1i 9	. 2 |- ( x e. A -> ( ph -> ps ) )
3	2	rexlimiv 2588	1 |- ( E. x e. A ph -> ps )

Syntax hints:   -> wi 4   e. wcel 2148   E.wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  r19.29vva  2622  eliun  3891  reusv3i  4460  elrnmptg  4880  fun11iun  5483  fmpt  5667  fliftfun  5797  elrnmpo  5988  releldm2  6186  tfrlem4  6314  iinerm  6607  elixpsn  6735  isfi  6761  cardcl  7180  cardval3ex  7184  ltbtwnnqq  7414  recexprlemlol  7625  recexprlemupu  7627  suplocsr  7808  restsspw  12698  ssnei  13654  tgcnp  13712  xmetunirn  13861  metss  13997  metrest  14009