Theorem rspcdv 3582

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086

This theorem is referenced by:  rspcdv2  3585  rspcv  3586  ralxfrd  5377  ralxfrd2  5381  reuop  6292  suppofss1d  8196  suppofss2d  8197  zindd  12693  wrd2ind  14756  ismri2dad  17689  mreexd  17694  mreexexlemd  17696  catcocl  17737  catass  17738  moni  17789  subccocl  17898  funcco  17924  fullfo  17967  fthf1  17972  nati  18011  chnind  18673  mndind  18883  ringurd  20263  idsrngd  20933  mpomulcn  24991  fsumdvdsmul  27321  uspgr2wlkeq  29932  crctcshwlkn0lem4  30099  crctcshwlkn0lem5  30100  wwlknllvtx  30132  0enwwlksnge1  30150  wlkiswwlks2lem5  30159  clwlkclwwlklem2a  30286  clwlkclwwlklem2  30288  clwwisshclwws  30303  clwwlkinwwlk  30328  umgr2cwwk2dif  30352  wrdt2ind  33210  mgccole1  33247  mgccole2  33248  mgcmnt1  33249  mgcmntco  33251  dfmgc2lem  33252  1arithufdlem3  33777  dfufd2  33781  fedgmullem2  33961  constrconj  34076  zart0  34210  zarcmplem  34212  esumcvg  34417  inelcarsg  34642  carsgclctunlem1  34648  orvcelel  34801  signsply0  34879  onint1  36845  qsalrel  42894  ismnushort  44898  ralbinrald  47743  fargshiftfva  48076  reupr  48155  evengpop3  48447  evengpoap3  48448  snlindsntorlem  49130