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  3916  reusv3i  4490  elrnmptg  4914  fun11iun  5521  fmpt  5708  fliftfun  5839  elrnmpo  6032  releldm2  6238  tfrlem4  6366  iinerm  6661  elixpsn  6789  isfi  6815  cardcl  7241  cardval3ex  7245  ltbtwnnqq  7475  recexprlemlol  7686  recexprlemupu  7688  suplocsr  7869  restsspw  12860  rhmdvdsr  13671  ssnei  14319  tgcnp  14377  xmetunirn  14526  metss  14662  metrest  14674