Theorem rspcdv 3583

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046

This theorem is referenced by:  rspcdv2  3586  rspcv  3587  ralxfrd  5366  ralxfrd2  5370  reuop  6269  suppofss1d  8186  suppofss2d  8187  zindd  12642  wrd2ind  14695  ismri2dad  17605  mreexd  17610  mreexexlemd  17612  catcocl  17653  catass  17654  moni  17705  subccocl  17814  funcco  17840  fullfo  17883  fthf1  17888  nati  17927  mndind  18762  ringurd  20101  idsrngd  20772  mpomulcn  24765  fsumdvdsmul  27112  uspgr2wlkeq  29581  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  wwlknllvtx  29783  0enwwlksnge1  29801  wlkiswwlks2lem5  29810  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwwisshclwws  29951  clwwlkinwwlk  29976  umgr2cwwk2dif  30000  wrdt2ind  32882  mgccole1  32923  mgccole2  32924  mgcmnt1  32925  mgcmntco  32927  dfmgc2lem  32928  chnind  32944  1arithufdlem3  33524  dfufd2  33528  fedgmullem2  33633  constrconj  33742  zart0  33876  zarcmplem  33878  esumcvg  34083  inelcarsg  34309  carsgclctunlem1  34315  orvcelel  34468  signsply0  34549  onint1  36444  qsalrel  42235  ismnushort  44297  ralbinrald  47127  fargshiftfva  47448  reupr  47527  evengpop3  47803  evengpoap3  47804  snlindsntorlem  48463