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 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2209  ∃wrex 2529

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

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

This theorem is referenced by:  r19.29vva  2696  eliun  4011  reusv3i  4600  elrnmptg  5029  fun11iun  5655  fmpt  5849  fliftfun  5992  elrnmpo  6192  releldm2  6409  tfrlem4  6574  iinerm  6871  elixpsn  7007  isfi  7037  cardcl  7516  cardval3ex  7520  ltbtwnnqq  7772  recexprlemlol  7983  recexprlemupu  7985  suplocsr  8166  restsspw  13580  rhmdvdsr  14455  ssnei  15175  tgcnp  15233  xmetunirn  15382  metss  15518  metrest  15530  clwwlknun  16596