Theorem rspcdv 3598

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

Hypotheses

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

Assertion

Ref	Expression
rspcdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))

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

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rspcdv

Step	Hyp	Ref	Expression
1		rspcdv.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		rspcdv.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))
3	2	biimpd 229	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))
4	1, 3	rspcimdv 3596	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053

This theorem is referenced by:  rspcdv2  3601  rspcv  3602  ralxfrd  5383  ralxfrd2  5387  reuop  6287  suppofss1d  8208  suppofss2d  8209  zindd  12699  wrd2ind  14746  ismri2dad  17654  mreexd  17659  mreexexlemd  17661  catcocl  17702  catass  17703  moni  17754  subccocl  17863  funcco  17889  fullfo  17932  fthf1  17937  nati  17976  mndind  18811  ringurd  20150  idsrngd  20821  mpomulcn  24814  fsumdvdsmul  27162  uspgr2wlkeq  29631  crctcshwlkn0lem4  29800  crctcshwlkn0lem5  29801  wwlknllvtx  29833  0enwwlksnge1  29851  wlkiswwlks2lem5  29860  clwlkclwwlklem2a  29984  clwlkclwwlklem2  29986  clwwisshclwws  30001  clwwlkinwwlk  30026  umgr2cwwk2dif  30050  wrdt2ind  32934  mgccole1  32975  mgccole2  32976  mgcmnt1  32977  mgcmntco  32979  dfmgc2lem  32980  chnind  32996  1arithufdlem3  33566  dfufd2  33570  fedgmullem2  33675  constrconj  33784  zart0  33915  zarcmplem  33917  esumcvg  34122  inelcarsg  34348  carsgclctunlem1  34354  orvcelel  34507  signsply0  34588  onint1  36472  qsalrel  42258  ismnushort  44292  ralbinrald  47118  fargshiftfva  47424  reupr  47503  evengpop3  47779  evengpoap3  47780  snlindsntorlem  48413