Theorem rspcdv 3573

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080

This theorem is referenced by:  rspcdv2  3576  rspcv  3577  ralxfrd  5379  ralxfrd2  5383  reuop  6294  suppofss1d  8196  suppofss2d  8197  zindd  12692  wrd2ind  14756  ismri2dad  17688  mreexd  17693  mreexexlemd  17695  catcocl  17736  catass  17737  moni  17788  subccocl  17897  funcco  17923  fullfo  17966  fthf1  17971  nati  18010  chnind  18672  mndind  18882  ringurd  20262  idsrngd  20959  mpomulcn  25026  fsumdvdsmul  27359  uspgr2wlkeq  29995  crctcshwlkn0lem4  30162  crctcshwlkn0lem5  30163  wwlknllvtx  30195  0enwwlksnge1  30213  wlkiswwlks2lem5  30222  clwlkclwwlklem2a  30349  clwlkclwwlklem2  30351  clwwisshclwws  30366  clwwlkinwwlk  30391  umgr2cwwk2dif  30415  wrdt2ind  33273  mgccole1  33310  mgccole2  33311  mgcmnt1  33312  mgcmntco  33314  dfmgc2lem  33315  1arithufdlem3  33836  dfufd2  33840  fedgmullem2  34020  constrconj  34135  zart0  34269  zarcmplem  34271  esumcvg  34476  inelcarsg  34701  carsgclctunlem1  34707  orvcelel  34860  signsply0  34938  onint1  36960  qsalrel  43009  ismnushort  45011  ralbinrald  47859  fargshiftfva  48192  reupr  48271  evengpop3  48563  evengpoap3  48564  snlindsntorlem  49250