Theorem rspcdv 3568

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  rspcdv2  3571  rspcv  3572  ralxfrd  5353  ralxfrd2  5357  reuop  6251  suppofss1d  8146  suppofss2d  8147  zindd  12593  wrd2ind  14646  ismri2dad  17560  mreexd  17565  mreexexlemd  17567  catcocl  17608  catass  17609  moni  17660  subccocl  17769  funcco  17795  fullfo  17838  fthf1  17843  nati  17882  chnind  18544  mndind  18753  ringurd  20120  idsrngd  20789  mpomulcn  24814  fsumdvdsmul  27161  uspgr2wlkeq  29719  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  wwlknllvtx  29919  0enwwlksnge1  29937  wlkiswwlks2lem5  29946  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwwisshclwws  30090  clwwlkinwwlk  30115  umgr2cwwk2dif  30139  wrdt2ind  33035  mgccole1  33072  mgccole2  33073  mgcmnt1  33074  mgcmntco  33076  dfmgc2lem  33077  1arithufdlem3  33627  dfufd2  33631  fedgmullem2  33787  constrconj  33902  zart0  34036  zarcmplem  34038  esumcvg  34243  inelcarsg  34468  carsgclctunlem1  34474  orvcelel  34627  signsply0  34708  onint1  36643  qsalrel  42496  ismnushort  44542  ralbinrald  47368  fargshiftfva  47689  reupr  47768  evengpop3  48044  evengpoap3  48045  snlindsntorlem  48716