Theorem rexlimivw 2735

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

Hypothesis

Ref	Expression
rexlimivw.1	⊢ (φ → ψ)

Assertion

Ref	Expression
rexlimivw	⊢ (∃x ∈ A φ → ψ)

Distinct variable group:   ψ,x

Allowed substitution hints:   φ(x)   A(x)

Proof of Theorem rexlimivw

Step	Hyp	Ref	Expression
1		rexlimivw.1	. . 3 ⊢ (φ → ψ)
2	1	a1i 10	. 2 ⊢ (x ∈ A → (φ → ψ))
3	2	rexlimiv 2733	1 ⊢ (∃x ∈ A φ → ψ)

Syntax hints:   → wi 4   ∈ wcel 1710  ∃wrex 2616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2620  df-rex 2621

This theorem is referenced by:  eliun  3974  eladdc  4399  tfinnnul  4491  phialllem1  4617  elima  4755  fun11iun  5306  fvelrnb  5366  fvelimab  5371  xpnedisj  5514  1st2nd2  5517  ovelrn  5609  fmpt  5693  enpw1  6063  eqtc  6162  addlec  6209  addceq0  6220  taddc  6230  nchoicelem14  6303  scancan  6332