Theorem rexlimivw 2647

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

Syntax hints:   → wi 4   ∈ wcel 2202  ∃wrex 2512

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516  df-rex 2517

This theorem is referenced by:  r19.29vva  2679  eliun  3979  reusv3i  4562  elrnmptg  4990  fun11iun  5613  fmpt  5805  fliftfun  5947  elrnmpo  6145  releldm2  6357  tfrlem4  6522  iinerm  6819  elixpsn  6947  isfi  6977  cardcl  7428  cardval3ex  7432  ltbtwnnqq  7678  recexprlemlol  7889  recexprlemupu  7891  suplocsr  8072  restsspw  13395  rhmdvdsr  14253  ssnei  14945  tgcnp  15003  xmetunirn  15152  metss  15288  metrest  15300  clwwlknun  16365