Theorem rexlimiv 2477

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

Syntax hints:   → wi 4   ∈ wcel 1434  ∃wrex 2354

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-i5r 1469

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2358  df-rex 2359

This theorem is referenced by:  rexlimiva  2478  rexlimivw  2479  rexlimivv  2488  r19.36av  2511  r19.44av  2519  r19.45av  2520  rexn0  3361  uniss2  3658  elres  4705  ssimaex  5310  tfrlem5  6011  tfrlem8  6015  ecoptocl  6309  mapsn  6377  findcard  6534  findcard2  6535  findcard2s  6536  prnmaddl  6952  0re  7391  cnegexlem2  7561  0cnALT  7575  bndndx  8564  uzn0  8929  ublbneg  8993  rexanuz2  10251  bj-inf2vnlem2  11209