Theorem rexlimiv 2732

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
rexlimiv.1	⊢ (x ∈ A → (φ → ψ))

Assertion

Ref	Expression
rexlimiv	⊢ (∃x ∈ A φ → ψ)

Distinct variable group:   ψ,x

Allowed substitution hints:   φ(x)   A(x)

Proof of Theorem rexlimiv

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 ⊢ Ⅎxψ
2		rexlimiv.1	. 2 ⊢ (x ∈ A → (φ → ψ))
3	1, 2	rexlimi 2731	1 ⊢ (∃x ∈ A φ → ψ)

Syntax hints:   → wi 4   ∈ wcel 1710  ∃wrex 2615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2619  df-rex 2620

This theorem is referenced by:  rexlimiva  2733  rexlimivw  2734  rexlimivv  2743  r19.36av  2759  r19.44av  2767  r19.45av  2768  rexn0  3652  uniss2  3922  pwadjoin  4119  nnc0suc  4412  lefinlteq  4463  ssfin  4470  evennn  4506  oddnn  4507  sucoddeven  4511  evenodddisj  4516  eventfin  4517  oddtfin  4518  fnasrn  5417  ecoptocl  5996  mapsn  6026  dflec3  6221  lenc  6223  taddc  6229  ce0tb  6238  ce0lenc1  6239  ncfin  6247  nncdiv3  6277  nchoicelem1  6289  nchoicelem2  6290  nchoicelem12  6300