Theorem rspcdv 3569

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rspcdv2  3572  rspcv  3573  ralxfrd  5347  ralxfrd2  5351  reuop  6241  suppofss1d  8137  suppofss2d  8138  zindd  12577  wrd2ind  14629  ismri2dad  17543  mreexd  17548  mreexexlemd  17550  catcocl  17591  catass  17592  moni  17643  subccocl  17752  funcco  17778  fullfo  17821  fthf1  17826  nati  17865  mndind  18702  ringurd  20070  idsrngd  20741  mpomulcn  24756  fsumdvdsmul  27103  uspgr2wlkeq  29591  crctcshwlkn0lem4  29758  crctcshwlkn0lem5  29759  wwlknllvtx  29791  0enwwlksnge1  29809  wlkiswwlks2lem5  29818  clwlkclwwlklem2a  29942  clwlkclwwlklem2  29944  clwwisshclwws  29959  clwwlkinwwlk  29984  umgr2cwwk2dif  30008  wrdt2ind  32895  mgccole1  32932  mgccole2  32933  mgcmnt1  32934  mgcmntco  32936  dfmgc2lem  32937  chnind  32953  1arithufdlem3  33483  dfufd2  33487  fedgmullem2  33597  constrconj  33712  zart0  33846  zarcmplem  33848  esumcvg  34053  inelcarsg  34279  carsgclctunlem1  34285  orvcelel  34438  signsply0  34519  onint1  36423  qsalrel  42213  ismnushort  44274  ralbinrald  47106  fargshiftfva  47427  reupr  47506  evengpop3  47782  evengpoap3  47783  snlindsntorlem  48455