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  4805  ralxfrdOLD  4806  ralxfrd2  4810  suppofss1d  7219  suppofss2d  7220  zindd  11354  wrd2ind  13329  ismri2dad  16120  mreexd  16125  mreexexlemd  16127  catcocl  16169  catass  16170  moni  16219  subccocl  16328  funcco  16354  fullfo  16395  fthf1  16400  nati  16438  mrcmndind  17189  idsrngd  18685  flfcntr  21657  sizeusglecusglem1  26012  fargshiftfva  26167  wlkiswwlk2lem5  26223  usg2wlkeq  26236  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwwisshclww  26335  usg2cwwk2dif  26348  eupatrl  26495  rngurd  29119  esumcvg  29475  inelcarsg  29700  carsgclctunlem1  29706  orvcelel  29858  signsply0  29954  onint1  31618  rspcdvinvd  37496  ralbinrald  39848  evengpop3  40214  evengpoap3  40215  uspgr2wlkeq  40854  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  0enwwlksnge1  41060  1wlkiswwlks2lem5  41070  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwwisshclwws  41235  umgr2cwwk2dif  41248  snlindsntorlem  42053