Theorem rexlimivw 2607

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

Syntax hints:   -> wi 4   e. wcel 2164   E.wrex 2473

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478

This theorem is referenced by:  r19.29vva  2639  eliun  3917  reusv3i  4491  elrnmptg  4915  fun11iun  5522  fmpt  5709  fliftfun  5840  elrnmpo  6033  releldm2  6240  tfrlem4  6368  iinerm  6663  elixpsn  6791  isfi  6817  cardcl  7243  cardval3ex  7247  ltbtwnnqq  7477  recexprlemlol  7688  recexprlemupu  7690  suplocsr  7871  restsspw  12863  rhmdvdsr  13674  ssnei  14330  tgcnp  14388  xmetunirn  14537  metss  14673  metrest  14685