Theorem rexlimivw 2583

Description: Weaker version of rexlimiv 2581. (Contributed by FL, 19-Sep-2011.)

Hypothesis

Ref	Expression
rexlimivw.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
rexlimivw	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimivw

Step	Hyp	Ref	Expression
1		rexlimivw.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 9	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	rexlimiv 2581	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2141  ∃wrex 2449

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  r19.29vva  2615  eliun  3875  reusv3i  4442  elrnmptg  4861  fun11iun  5461  fmpt  5643  fliftfun  5772  elrnmpo  5963  releldm2  6161  tfrlem4  6289  iinerm  6581  elixpsn  6709  isfi  6735  cardcl  7145  cardval3ex  7149  ltbtwnnqq  7364  recexprlemlol  7575  recexprlemupu  7577  suplocsr  7758  restsspw  12576  ssnei  12904  tgcnp  12962  xmetunirn  13111  metss  13247  metrest  13259