Theorem rexlimiv 2608

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

Syntax hints:   → wi 4   ∈ wcel 2167  ∃wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  rexlimiva  2609  rexlimivw  2610  rexlimivv  2620  r19.36av  2648  r19.44av  2656  r19.45av  2657  rexn0  3550  uniss2  3871  elres  4983  ssimaex  5625  mpoexw  6280  tfrlem5  6381  tfrlem8  6385  ecoptocl  6690  mapsn  6758  elixpsn  6803  ixpsnf1o  6804  findcard  6958  findcard2  6959  findcard2s  6960  fiintim  7001  prnmaddl  7576  0re  8045  cnegexlem2  8221  0cnALT  8235  bndndx  9267  uzn0  9636  ublbneg  9706  rexanuz2  11175  opnneiid  14508  2lgslem1b  15438  2sqlem2  15464  bj-inf2vnlem2  15725