Theorem rexlimivw 2620

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

Syntax hints:   → wi 4   ∈ wcel 2177  ∃wrex 2486

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2490  df-rex 2491

This theorem is referenced by:  r19.29vva  2652  eliun  3940  reusv3i  4519  elrnmptg  4944  fun11iun  5560  fmpt  5748  fliftfun  5883  elrnmpo  6077  releldm2  6289  tfrlem4  6417  iinerm  6712  elixpsn  6840  isfi  6870  cardcl  7309  cardval3ex  7313  ltbtwnnqq  7558  recexprlemlol  7769  recexprlemupu  7771  suplocsr  7952  restsspw  13166  rhmdvdsr  14022  ssnei  14708  tgcnp  14766  xmetunirn  14915  metss  15051  metrest  15063