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  7527  cardval3ex  7531  ltbtwnnqq  7783  recexprlemlol  7994  recexprlemupu  7996  suplocsr  8177  restsspw  13656  rhmdvdsr  14566  ssnei  15343  tgcnp  15401  xmetunirn  15550  metss  15686  metrest  15698  clwwlknun  16848