Theorem rexlimivw 2646

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  r19.29vva  2678  eliun  3974  reusv3i  4556  elrnmptg  4984  fun11iun  5604  fmpt  5797  fliftfun  5936  elrnmpo  6134  releldm2  6347  tfrlem4  6478  iinerm  6775  elixpsn  6903  isfi  6933  cardcl  7384  cardval3ex  7388  ltbtwnnqq  7634  recexprlemlol  7845  recexprlemupu  7847  suplocsr  8028  restsspw  13331  rhmdvdsr  14188  ssnei  14874  tgcnp  14932  xmetunirn  15081  metss  15217  metrest  15229  clwwlknun  16291