Theorem rspcdv 3627

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068

This theorem is referenced by:  rspcdv2  3630  rspcv  3631  ralxfrd  5426  ralxfrd2  5430  reuop  6324  suppofss1d  8245  suppofss2d  8246  zindd  12744  wrd2ind  14771  ismri2dad  17695  mreexd  17700  mreexexlemd  17702  catcocl  17743  catass  17744  moni  17797  subccocl  17909  funcco  17935  fullfo  17979  fthf1  17984  nati  18023  mndind  18863  ringurd  20212  idsrngd  20879  mpomulcn  24910  fsumdvdsmul  27256  uspgr2wlkeq  29682  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  wwlknllvtx  29879  0enwwlksnge1  29897  wlkiswwlks2lem5  29906  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwwisshclwws  30047  clwwlkinwwlk  30072  umgr2cwwk2dif  30096  wrdt2ind  32920  mgccole1  32963  mgccole2  32964  mgcmnt1  32965  mgcmntco  32967  dfmgc2lem  32968  chnind  32983  1arithufdlem3  33539  dfufd2  33543  fedgmullem2  33643  constrconj  33735  zart0  33825  zarcmplem  33827  esumcvg  34050  inelcarsg  34276  carsgclctunlem1  34282  orvcelel  34434  signsply0  34528  onint1  36415  qsalrel  42235  ismnushort  44270  ralbinrald  47037  fargshiftfva  47317  reupr  47396  evengpop3  47672  evengpoap3  47673  snlindsntorlem  48199