Theorem rspcdv 3552

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054

This theorem is referenced by:  rspcdv2  3555  rspcv  3556  ralxfrd  5337  ralxfrd2  5341  reuop  6244  suppofss1d  8144  suppofss2d  8145  zindd  12621  wrd2ind  14676  ismri2dad  17594  mreexd  17599  mreexexlemd  17601  catcocl  17642  catass  17643  moni  17694  subccocl  17803  funcco  17829  fullfo  17872  fthf1  17877  nati  17916  chnind  18578  mndind  18787  ringurd  20157  idsrngd  20828  mpomulcn  24852  fsumdvdsmul  27176  uspgr2wlkeq  29732  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  wwlknllvtx  29932  0enwwlksnge1  29950  wlkiswwlks2lem5  29959  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwwisshclwws  30103  clwwlkinwwlk  30128  umgr2cwwk2dif  30152  wrdt2ind  33032  mgccole1  33069  mgccole2  33070  mgcmnt1  33071  mgcmntco  33073  dfmgc2lem  33074  1arithufdlem3  33629  dfufd2  33633  fedgmullem2  33814  constrconj  33929  zart0  34063  zarcmplem  34065  esumcvg  34270  inelcarsg  34495  carsgclctunlem1  34501  orvcelel  34654  signsply0  34735  onint1  36677  qsalrel  42725  ismnushort  44745  ralbinrald  47585  fargshiftfva  47918  reupr  47997  evengpop3  48289  evengpoap3  48290  snlindsntorlem  48961