Theorem rexlimdv 2548

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 1508	. 2 ⊢ Ⅎ𝑥𝜑
2		nfv 1508	. 2 ⊢ Ⅎ𝑥𝜒
3		rexlimdv.1	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
4	1, 2, 3	rexlimd 2546	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∈ wcel 1480  ∃wrex 2417

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421  df-rex 2422

This theorem is referenced by:  rexlimdva  2549  rexlimdv3a  2551  rexlimdva2  2552  rexlimdvw  2553  rexlimdvv  2556  ssorduni  4403  funcnvuni  5192  dffo3  5567  smoiun  6198  tfrlem9  6216  ordiso2  6920  axprecex  7688  recexap  8414  zdiv  9139  btwnz  9170  lbzbi  9408  neibl  12660  metcnp3  12680