Theorem rexlimivw 2579

Description: Weaker version of rexlimiv 2577. (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 2577	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2136  ∃wrex 2445

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449  df-rex 2450

This theorem is referenced by:  r19.29vva  2611  eliun  3870  reusv3i  4437  elrnmptg  4856  fun11iun  5453  fmpt  5635  fliftfun  5764  elrnmpo  5955  releldm2  6153  tfrlem4  6281  iinerm  6573  elixpsn  6701  isfi  6727  cardcl  7137  cardval3ex  7141  ltbtwnnqq  7356  recexprlemlol  7567  recexprlemupu  7569  suplocsr  7750  restsspw  12566  ssnei  12791  tgcnp  12849  xmetunirn  12998  metss  13134  metrest  13146