Theorem rexlimdva 2738

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)

Hypothesis

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

Assertion

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

Distinct variable groups:   φ,x   χ,x

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

Proof of Theorem rexlimdva

Step	Hyp	Ref	Expression
1		rexlimdva.1	. . 3 ⊢ ((φ ∧ x ∈ A) → (ψ → χ))
2	1	ex 423	. 2 ⊢ (φ → (x ∈ A → (ψ → χ)))
3	2	rexlimdv 2737	1 ⊢ (φ → (∃x ∈ A ψ → χ))

Syntax hints:   → wi 4   ∧ wa 358   ∈ 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:  rexlimdvaa  2739  rexlimivv  2743  rexlimdvv  2744  pw1disj  4167  leltfintr  4458  ncfinlower  4483  tfin11  4493  tfinpw1  4494  nnpweq  4523  sfin112  4529  sfindbl  4530  vfinspss  4551  vfinspeqtncv  4553  phi11lem1  4595  foco2  5426  f1elima  5474  ectocld  5991  ncssfin  6151  nntccl  6170  dflec2  6210  leaddc1  6214  leconnnc  6218  tlecg  6230  letc  6231  ce2le  6233  ce0lenc1  6239  nclenn  6249  lemuc1  6253  lecadd2  6266  ncslesuc  6267  nnc3n3p1  6278  nchoicelem17  6305  nchoicelem19  6307  nchoice  6308  dmfrec  6316  fnfreclem3  6319