Theorem rexlimivw 2474

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

Syntax hints:   -> wi 4   e. wcel 1434   E.wrex 2350

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-i5r 1469

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354  df-rex 2355

This theorem is referenced by:  r19.29vva  2501  eliun  3690  reusv3i  4217  elrnmptg  4614  fun11iun  5178  fmpt  5351  fliftfun  5467  elrnmpt2  5645  releldm2  5842  tfrlem4  5962  iinerm  6244  isfi  6308  cardcl  6509  cardval3ex  6513  ltbtwnnqq  6667  recexprlemlol  6878  recexprlemupu  6880