Theorem rspcedv 3583

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 3581	1 ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096

This theorem is referenced by:  rspcebdv  3584  rspcev  3590  rspcedvd  3592  0csh0  14829  gcdcllem1  16556  nn0gsumfz  20053  pmatcollpw3lem  22908  pmatcollpw3fi1lem2  22912  pm2mpfo  22939  f1otrg  29160  cusgrfilem2  29746  wwlksnredwwlkn  30184  wwlksnextprop  30201  clwwlknun  30403  cusconngr  30482  xrofsup  33052  esum2d  34427  rexzrexnn0  43422  onsucelab  43881  ordnexbtwnsuc  43885  ov2ssiunov2  44317  requad2  48276  lcoel0  49092  lcoss  49100  el0ldep  49130  ldepspr  49137  islindeps2  49147  isldepslvec2  49149  affinecomb1  49366  isisod  49689