Theorem rexlimiv 2618

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

Syntax hints:   → wi 4   ∈ wcel 2177  ∃wrex 2486

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2490  df-rex 2491

This theorem is referenced by:  rexlimiva  2619  rexlimivw  2620  rexlimivv  2630  r19.36av  2658  r19.44av  2666  r19.45av  2667  rexn0  3563  uniss2  3887  elres  5004  ssimaex  5653  mpoexw  6312  tfrlem5  6413  tfrlem8  6417  ecoptocl  6722  mapsn  6790  elixpsn  6835  ixpsnf1o  6836  findcard  7000  findcard2  7001  findcard2s  7002  fiintim  7043  prnmaddl  7623  0re  8092  cnegexlem2  8268  0cnALT  8282  bndndx  9314  uzn0  9684  ublbneg  9754  rexanuz2  11377  opnneiid  14711  2lgslem1b  15641  2sqlem2  15667  bj-inf2vnlem2  16045