Theorem rspcdv 3572

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 231	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))
4	1, 3	rspcimdv 3570	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076

This theorem is referenced by:  rspcdv2  3575  rspcv  3576  ralxfrd  5362  ralxfrd2  5366  reuop  6275  suppofss1d  8178  suppofss2d  8179  zindd  12668  wrd2ind  14730  ismri2dad  17660  mreexd  17665  mreexexlemd  17667  catcocl  17708  catass  17709  moni  17760  subccocl  17869  funcco  17895  fullfo  17938  fthf1  17943  nati  17982  chnind  18644  mndind  18853  ringurd  20222  idsrngd  20893  mpomulcn  24917  fsumdvdsmul  27247  uspgr2wlkeq  29803  crctcshwlkn0lem4  29970  crctcshwlkn0lem5  29971  wwlknllvtx  30003  0enwwlksnge1  30021  wlkiswwlks2lem5  30030  clwlkclwwlklem2a  30157  clwlkclwwlklem2  30159  clwwisshclwws  30174  clwwlkinwwlk  30199  umgr2cwwk2dif  30223  wrdt2ind  33092  mgccole1  33129  mgccole2  33130  mgcmnt1  33131  mgcmntco  33133  dfmgc2lem  33134  1arithufdlem3  33703  dfufd2  33707  fedgmullem2  33888  constrconj  34003  zart0  34137  zarcmplem  34139  esumcvg  34344  inelcarsg  34569  carsgclctunlem1  34575  orvcelel  34728  signsply0  34806  onint1  36770  qsalrel  42818  ismnushort  44838  ralbinrald  47677  fargshiftfva  48010  reupr  48089  evengpop3  48381  evengpoap3  48382  snlindsntorlem  49053