Theorem rspcdv 3614

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060

This theorem is referenced by:  rspcdv2  3617  rspcv  3618  ralxfrd  5414  ralxfrd2  5418  reuop  6315  suppofss1d  8228  suppofss2d  8229  zindd  12717  wrd2ind  14758  ismri2dad  17682  mreexd  17687  mreexexlemd  17689  catcocl  17730  catass  17731  moni  17784  subccocl  17896  funcco  17922  fullfo  17966  fthf1  17971  nati  18010  mndind  18854  ringurd  20203  idsrngd  20874  mpomulcn  24905  fsumdvdsmul  27253  uspgr2wlkeq  29679  crctcshwlkn0lem4  29843  crctcshwlkn0lem5  29844  wwlknllvtx  29876  0enwwlksnge1  29894  wlkiswwlks2lem5  29903  clwlkclwwlklem2a  30027  clwlkclwwlklem2  30029  clwwisshclwws  30044  clwwlkinwwlk  30069  umgr2cwwk2dif  30093  wrdt2ind  32923  mgccole1  32965  mgccole2  32966  mgcmnt1  32967  mgcmntco  32969  dfmgc2lem  32970  chnind  32985  1arithufdlem3  33554  dfufd2  33558  fedgmullem2  33658  constrconj  33750  zart0  33840  zarcmplem  33842  esumcvg  34067  inelcarsg  34293  carsgclctunlem1  34299  orvcelel  34451  signsply0  34545  onint1  36432  qsalrel  42260  ismnushort  44297  ralbinrald  47072  fargshiftfva  47368  reupr  47447  evengpop3  47723  evengpoap3  47724  snlindsntorlem  48316