Theorem rexlimiv 2601

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 1539	. 2 ⊢ Ⅎ𝑥𝜓
2		rexlimiv.1	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	1, 2	rexlimi 2600	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2160  ∃wrex 2469

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473  df-rex 2474

This theorem is referenced by:  rexlimiva  2602  rexlimivw  2603  rexlimivv  2613  r19.36av  2641  r19.44av  2649  r19.45av  2650  rexn0  3536  uniss2  3855  elres  4961  ssimaex  5597  mpoexw  6237  tfrlem5  6338  tfrlem8  6342  ecoptocl  6647  mapsn  6715  elixpsn  6760  ixpsnf1o  6761  findcard  6915  findcard2  6916  findcard2s  6917  fiintim  6956  prnmaddl  7518  0re  7986  cnegexlem2  8162  0cnALT  8176  bndndx  9204  uzn0  9572  ublbneg  9642  rexanuz2  11031  opnneiid  14116  2sqlem2  14915  bj-inf2vnlem2  15176