Theorem rexlimivw 2664

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  r19.29vva  2696  eliun  4016  reusv3i  4605  elrnmptg  5034  fun11iun  5660  fmpt  5858  fliftfun  6002  elrnmpo  6202  releldm2  6419  tfrlem4  6584  iinerm  6881  elixpsn  7017  isfi  7047  cardcl  7526  cardval3ex  7530  ltbtwnnqq  7782  recexprlemlol  7993  recexprlemupu  7995  suplocsr  8176  restsspw  13603  rhmdvdsr  14482  ssnei  15252  tgcnp  15310  xmetunirn  15459  metss  15595  metrest  15607  clwwlknun  16682