Theorem rspcdv 3285

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175

This theorem is referenced by:  rspcdva  3288  ralxfrd  4800  ralxfrdOLD  4801  ralxfrd2  4805  suppofss1d  7197  suppofss2d  7198  zindd  11313  wrd2ind  13278  ismri2dad  16069  mreexd  16074  mreexexlemd  16076  catcocl  16118  catass  16119  moni  16168  subccocl  16277  funcco  16303  fullfo  16344  fthf1  16349  nati  16387  mrcmndind  17138  idsrngd  18634  flfcntr  21605  sizeusglecusglem1  25806  fargshiftfva  25961  wlkiswwlk2lem5  26017  usg2wlkeq  26030  clwlkisclwwlklem2a  26107  clwlkisclwwlklem1  26109  clwwisshclww  26129  usg2cwwk2dif  26142  eupatrl  26289  rngurd  28913  esumcvg  29269  inelcarsg  29494  carsgclctunlem1  29500  orvcelel  29652  signsply0  29748  onint1  31412  rspcdvinvd  37290  ralbinrald  39642  evengpop3  40009  evengpoap3  40010  uspgr2wlkeq  40846  crctcsh1wlkn0lem4  41008  crctcsh1wlkn0lem5  41009  0enwwlksnge1  41052  1wlkiswwlks2lem5  41062  clwlkclwwlklem2a  41199  clwlkclwwlklem2  41201  clwwisshclwws  41227  umgr2cwwk2dif  41240  snlindsntorlem  42045