Theorem rspcdv 3564

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048

This theorem is referenced by:  rspcdv2  3567  rspcv  3568  ralxfrd  5341  ralxfrd2  5345  reuop  6235  suppofss1d  8129  suppofss2d  8130  zindd  12569  wrd2ind  14625  ismri2dad  17538  mreexd  17543  mreexexlemd  17545  catcocl  17586  catass  17587  moni  17638  subccocl  17747  funcco  17773  fullfo  17816  fthf1  17821  nati  17860  chnind  18522  mndind  18731  ringurd  20098  idsrngd  20766  mpomulcn  24780  fsumdvdsmul  27127  uspgr2wlkeq  29619  crctcshwlkn0lem4  29786  crctcshwlkn0lem5  29787  wwlknllvtx  29819  0enwwlksnge1  29837  wlkiswwlks2lem5  29846  clwlkclwwlklem2a  29970  clwlkclwwlklem2  29972  clwwisshclwws  29987  clwwlkinwwlk  30012  umgr2cwwk2dif  30036  wrdt2ind  32926  mgccole1  32963  mgccole2  32964  mgcmnt1  32965  mgcmntco  32967  dfmgc2lem  32968  1arithufdlem3  33503  dfufd2  33507  fedgmullem2  33635  constrconj  33750  zart0  33884  zarcmplem  33886  esumcvg  34091  inelcarsg  34316  carsgclctunlem1  34322  orvcelel  34475  signsply0  34556  onint1  36483  qsalrel  42273  ismnushort  44334  ralbinrald  47153  fargshiftfva  47474  reupr  47553  evengpop3  47829  evengpoap3  47830  snlindsntorlem  48502