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  3549  uniss2  3870  elres  4982  ssimaex  5622  mpoexw  6271  tfrlem5  6372  tfrlem8  6376  ecoptocl  6681  mapsn  6749  elixpsn  6794  ixpsnf1o  6795  findcard  6949  findcard2  6950  findcard2s  6951  fiintim  6992  prnmaddl  7557  0re  8026  cnegexlem2  8202  0cnALT  8216  bndndx  9248  uzn0  9617  ublbneg  9687  rexanuz2  11156  opnneiid  14400  2lgslem1b  15330  2sqlem2  15356  bj-inf2vnlem2  15617