Theorem rexlimivw 2734

Description: Weaker version of rexlimiv 2732. (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 2732	1 ⊢ (∃x ∈ A φ → ψ)

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

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 2619  df-rex 2620

This theorem is referenced by:  eliun  3973  eladdc  4398  tfinnnul  4490  phialllem1  4616  elima  4754  fun11iun  5305  fvelrnb  5365  fvelimab  5370  xpnedisj  5513  1st2nd2  5516  ovelrn  5608  fmpt  5692  enpw1  6062  eqtc  6161  addlec  6208  addceq0  6219  taddc  6229  nchoicelem14  6302  scancan  6331