Theorem rspcedv 3554

Description: Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)

Hypotheses

Ref	Expression
rspcdv.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
rspcdv.2	⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rspcedv	⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥   𝜒,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rspcedv

Step	Hyp	Ref	Expression
1		rspcdv.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		rspcdv.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))
3	2	biimprd 247	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))
4	1, 3	rspcimedv 3552	1 ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070

This theorem is referenced by:  rspcebdv  3555  rspcev  3561  rspcedvd  3563  0csh0  14506  gcdcllem1  16206  nn0gsumfz  19585  pmatcollpw3lem  21932  pmatcollpw3fi1lem2  21936  pm2mpfo  21963  f1otrg  27232  cusgrfilem2  27823  wwlksnredwwlkn  28260  wwlksnextprop  28277  clwwlknun  28476  cusconngr  28555  xrofsup  31090  esum2d  32061  rexzrexnn0  40626  ov2ssiunov2  41308  requad2  45075  lcoel0  45769  lcoss  45777  el0ldep  45807  ldepspr  45814  islindeps2  45824  isldepslvec2  45826  affinecomb1  46048