Theorem rexlimivw 2646

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

Syntax hints:   -> wi 4   e. wcel 2202   E.wrex 2511

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  r19.29vva  2678  eliun  3974  reusv3i  4556  elrnmptg  4984  fun11iun  5604  fmpt  5797  fliftfun  5937  elrnmpo  6135  releldm2  6348  tfrlem4  6479  iinerm  6776  elixpsn  6904  isfi  6934  cardcl  7385  cardval3ex  7389  ltbtwnnqq  7635  recexprlemlol  7846  recexprlemupu  7848  suplocsr  8029  restsspw  13350  rhmdvdsr  14208  ssnei  14894  tgcnp  14952  xmetunirn  15101  metss  15237  metrest  15249  clwwlknun  16311