Theorem rspcdv 3614

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-ral 3143

This theorem is referenced by:  rspcv  3617  ralxfrd  5300  ralxfrd2  5304  reuop  6138  suppofss1d  7862  suppofss2d  7863  zindd  12077  wrd2ind  14079  ismri2dad  16902  mreexd  16907  mreexexlemd  16909  catcocl  16950  catass  16951  moni  17000  subccocl  17109  funcco  17135  fullfo  17176  fthf1  17181  nati  17219  mndind  17986  idsrngd  19627  uspgr2wlkeq  27421  crctcshwlkn0lem4  27585  crctcshwlkn0lem5  27586  wwlknllvtx  27618  0enwwlksnge1  27636  wlkiswwlks2lem5  27645  clwlkclwwlklem2a  27770  clwlkclwwlklem2  27772  clwwisshclwws  27787  clwwlkinwwlk  27812  umgr2cwwk2dif  27837  wrdt2ind  30622  rngurd  30852  fedgmullem2  31021  esumcvg  31340  inelcarsg  31564  carsgclctunlem1  31570  orvcelel  31722  signsply0  31816  onint1  33792  qsalrel  39118  rspcdvinvd  40517  ralbinrald  43315  fargshiftfva  43597  reupr  43678  evengpop3  43957  evengpoap3  43958  isomgrsym  43995  snlindsntorlem  44519