Theorem rexlimivw 2583

Description: Weaker version of rexlimiv 2581. (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 2581	1 |- ( E. x e. A ph -> ps )

Syntax hints:   -> wi 4   e. wcel 2141   E.wrex 2449

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  r19.29vva  2615  eliun  3877  reusv3i  4444  elrnmptg  4863  fun11iun  5463  fmpt  5646  fliftfun  5775  elrnmpo  5966  releldm2  6164  tfrlem4  6292  iinerm  6585  elixpsn  6713  isfi  6739  cardcl  7158  cardval3ex  7162  ltbtwnnqq  7377  recexprlemlol  7588  recexprlemupu  7590  suplocsr  7771  restsspw  12589  ssnei  12945  tgcnp  13003  xmetunirn  13152  metss  13288  metrest  13300