Theorem rexlimivw 2618

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

Syntax hints:   → wi 4   ∈ wcel 2175  ∃wrex 2484

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-i5r 1557

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-ral 2488  df-rex 2489

This theorem is referenced by:  r19.29vva  2650  eliun  3930  reusv3i  4505  elrnmptg  4929  fun11iun  5542  fmpt  5729  fliftfun  5864  elrnmpo  6058  releldm2  6270  tfrlem4  6398  iinerm  6693  elixpsn  6821  isfi  6851  cardcl  7287  cardval3ex  7291  ltbtwnnqq  7527  recexprlemlol  7738  recexprlemupu  7740  suplocsr  7921  restsspw  13023  rhmdvdsr  13879  ssnei  14565  tgcnp  14623  xmetunirn  14772  metss  14908  metrest  14920