Theorem rexlimiv 2588

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
rexlimiv.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

Ref	Expression
rexlimiv	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiv

Step	Hyp	Ref	Expression
1		nfv 1528	. 2 ⊢ Ⅎ𝑥𝜓
2		rexlimiv.1	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	1, 2	rexlimi 2587	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  rexlimiva  2589  rexlimivw  2590  rexlimivv  2600  r19.36av  2628  r19.44av  2636  r19.45av  2637  rexn0  3521  uniss2  3839  elres  4940  ssimaex  5574  mpoexw  6209  tfrlem5  6310  tfrlem8  6314  ecoptocl  6617  mapsn  6685  elixpsn  6730  ixpsnf1o  6731  findcard  6883  findcard2  6884  findcard2s  6885  fiintim  6923  prnmaddl  7484  0re  7952  cnegexlem2  8127  0cnALT  8141  bndndx  9169  uzn0  9537  ublbneg  9607  rexanuz2  10991  opnneiid  13446  2sqlem2  14233  bj-inf2vnlem2  14494