Theorem rexlimivw 2647

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

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

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  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516  df-rex 2517

This theorem is referenced by:  r19.29vva  2679  eliun  3979  reusv3i  4562  elrnmptg  4990  fun11iun  5613  fmpt  5805  fliftfun  5947  elrnmpo  6145  releldm2  6357  tfrlem4  6522  iinerm  6819  elixpsn  6947  isfi  6977  cardcl  7445  cardval3ex  7449  ltbtwnnqq  7695  recexprlemlol  7906  recexprlemupu  7908  suplocsr  8089  restsspw  13412  rhmdvdsr  14270  ssnei  14962  tgcnp  15020  xmetunirn  15169  metss  15305  metrest  15317  clwwlknun  16382