Theorem rexlimdvaa 2661

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypothesis

Ref	Expression
rexlimdvaa.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

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

Proof of Theorem rexlimdvaa

Step	Hyp	Ref	Expression
1		rexlimdvaa.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
2	1	expr 375	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	rexlimdva 2660	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  ∃wrex 2521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525  df-rex 2526

This theorem is referenced by:  rexlimddv  2665  nnsucuniel  6727  omp1eomlem  7384  ctmlemr  7398  mulgt0sr  8092  axpre-suploclemres  8215  cnegex  8450  receuap  8942  recapb  8944  rexanuz  11669  climcaucn  12032  fsumiun  12159  dvdsval2  12472  nninfctlemfo  12732  prmind2  12813  pcprmpw2  13027  pockthg  13051  dvdsrvald  14230  dvdsrd  14231  dvdsrex  14235  unitgrp  14253  isnzr2  14321  znunit  14799  tgcl  14921  neiint  15002  restopnb  15038  iscnp4  15075  blssexps  15286  blssex  15287  lgsne0  15903  lgsquadlem1  15942