Theorem rexlimivw 2664

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  r19.29vva  2696  eliun  4016  reusv3i  4607  elrnmptg  5036  fun11iun  5663  fmpt  5861  fliftfun  6005  elrnmpo  6205  releldm2  6423  tfrlem4  6588  iinerm  6885  elixpsn  7021  isfi  7051  cardcl  7532  cardval3ex  7536  ltbtwnnqq  7788  recexprlemlol  7999  recexprlemupu  8001  suplocsr  8182  restsspw  13662  rhmdvdsr  14591  ssnei  15377  tgcnp  15435  xmetunirn  15584  metss  15720  metrest  15732  clwwlknun  16887