Theorem rexlimdv 2551

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	⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))

Assertion

Ref	Expression
rexlimdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdv

Step	Hyp	Ref	Expression
1		nfv 1509	. 2 ⊢ Ⅎ𝑥𝜑
2		nfv 1509	. 2 ⊢ Ⅎ𝑥𝜒
3		rexlimdv.1	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
4	1, 2, 3	rexlimd 2549	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∈ wcel 1481  ∃wrex 2418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-i5r 1516

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422  df-rex 2423

This theorem is referenced by:  rexlimdva  2552  rexlimdv3a  2554  rexlimdva2  2555  rexlimdvw  2556  rexlimdvv  2559  ssorduni  4411  funcnvuni  5200  dffo3  5575  smoiun  6206  tfrlem9  6224  ordiso2  6928  axprecex  7712  recexap  8438  zdiv  9163  btwnz  9194  lbzbi  9435  neibl  12699  metcnp3  12719