Theorem rexlimivw 2567

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

Syntax hints:   -> wi 4   e. wcel 2125   E.wrex 2433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511  ax-i5r 1512

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2437  df-rex 2438

This theorem is referenced by:  r19.29vva  2599  eliun  3849  reusv3i  4413  elrnmptg  4831  fun11iun  5428  fmpt  5610  fliftfun  5737  elrnmpo  5924  releldm2  6123  tfrlem4  6250  iinerm  6541  elixpsn  6669  isfi  6695  cardcl  7095  cardval3ex  7099  ltbtwnnqq  7314  recexprlemlol  7525  recexprlemupu  7527  suplocsr  7708  restsspw  12300  ssnei  12490  tgcnp  12548  xmetunirn  12697  metss  12833  metrest  12845