Theorem rspcdv 3569

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078

This theorem is used by:  rspcdv2  3572  rspcv  3573  ralxfrd  5370  ralxfrd2  5374  reuop  6295  suppofss1d  8214  suppofss2d  8215  zindd  12793  wrd2ind  14865  ismri2dad  17804  mreexd  17809  mreexexlemd  17811  catcocl  17852  catass  17853  moni  17904  subccocl  18013  funcco  18039  fullfo  18082  fthf1  18087  nati  18126  chnind  18788  mndind  19017  ringurd  20404  idsrngd  21106  mpomulcn  25181  fsumdvdsmul  27515  uspgr2wlkeq  30219  crctcshwlkn0lem4  30395  crctcshwlkn0lem5  30396  wwlknllvtx  30428  0enwwlksnge1  30446  wlkiswwlks2lem5  30455  clwlkclwwlklem2a  30582  clwlkclwwlklem2  30584  clwwisshclwws  30599  clwwlkinwwlk  30624  umgr2cwwk2dif  30648  wrdt2ind  33509  mgccole1  33544  mgccole2  33545  mgcmnt1  33546  mgcmntco  33548  dfmgc2lem  33549  1arithufdlem3  34071  dfufd2  34075  fedgmullem2  34255  constrconj  34370  zart0  34504  zarcmplem  34506  esumcvg  34711  inelcarsg  34936  carsgclctunlem1  34942  orvcelel  35095  signsply0  35173  onint1  37217  qsalrel  43272  ismnushort  45270  ralbinrald  48161  fargshiftfva  48494  reupr  48573  evengpop3  48865  evengpoap3  48866  snlindsntorlem  49551