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 1570   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  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  14864  gcdcllem1  16589  nn0gsumfz  20111  pmatcollpw3lem  23008  pmatcollpw3fi1lem2  23012  pm2mpfo  23039  f1otrg  29327  cusgrfilem2  29916  wwlksnredwwlkn  30363  wwlksnextprop  30380  clwwlknun  30582  cusconngr  30671  xrofsup  33238  esum2d  34603  rexzrexnn0  43645  onsucelab  44104  ordnexbtwnsuc  44108  ov2ssiunov2  44540  requad2  48539  lcoel0  49358  lcoss  49366  el0ldep  49396  ldepspr  49403  islindeps2  49413  isldepslvec2  49415  affinecomb1  49632  isisod  49953