Theorem rexlimdv 2737

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis

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

Assertion

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

Distinct variable groups:   φ,x   χ,x

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

Proof of Theorem rexlimdv

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 ⊢ Ⅎxφ
2		nfv 1619	. 2 ⊢ Ⅎxχ
3		rexlimdv.1	. 2 ⊢ (φ → (x ∈ A → (ψ → χ)))
4	1, 2, 3	rexlimd 2735	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:  rexlimdva  2738  rexlimdv3a  2740  rexlimdvw  2741  rexlimdvv  2744  eqpw1uni  4330  nndisjeq  4429  ssfin  4470  nnpw1ex  4484  tfinltfinlem1  4500  sfin112  4529  sfintfin  4532  sfinltfin  4535  funcnvuni  5161  dffo3  5422  nclenn  6249  ncslesuc  6267