Theorem rspcedv 3569

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 251	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))
4	1, 3	rspcimedv 3567	1 ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087

This theorem is used by:  rspcebdv  3570  rspcev  3576  rspcedvd  3578  0csh0  14952  gcdcllem1  16678  nn0gsumfz  20207  pmatcollpw3lem  23110  pmatcollpw3fi1lem2  23114  pm2mpfo  23141  f1otrg  29457  cusgrfilem2  30046  wwlksnredwwlkn  30493  wwlksnextprop  30510  clwwlknun  30712  cusconngr  30801  xrofsup  33409  esum2d  34775  rexzrexnn0  43920  onsucelab  44374  ordnexbtwnsuc  44378  ov2ssiunov2  44809  requad2  48829  lcoel0  49648  lcoss  49656  el0ldep  49686  ldepspr  49693  islindeps2  49703  isldepslvec2  49705  affinecomb1  49922  isisod  50249