Theorem rspcdv 3604

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062

This theorem is referenced by:  rspcdv2  3607  rspcv  3608  ralxfrd  5406  ralxfrd2  5410  reuop  6292  suppofss1d  8191  suppofss2d  8192  zindd  12667  wrd2ind  14677  ismri2dad  17585  mreexd  17590  mreexexlemd  17592  catcocl  17633  catass  17634  moni  17687  subccocl  17799  funcco  17825  fullfo  17867  fthf1  17872  nati  17910  mndind  18745  ringurd  20079  idsrngd  20613  mpomulcn  24605  uspgr2wlkeq  29158  crctcshwlkn0lem4  29322  crctcshwlkn0lem5  29323  wwlknllvtx  29355  0enwwlksnge1  29373  wlkiswwlks2lem5  29382  clwlkclwwlklem2a  29506  clwlkclwwlklem2  29508  clwwisshclwws  29523  clwwlkinwwlk  29548  umgr2cwwk2dif  29572  wrdt2ind  32372  mgccole1  32415  mgccole2  32416  mgcmnt1  32417  mgcmntco  32419  dfmgc2lem  32420  fedgmullem2  32991  zart0  33145  zarcmplem  33147  esumcvg  33370  inelcarsg  33596  carsgclctunlem1  33602  orvcelel  33754  signsply0  33848  onint1  35637  qsalrel  41368  ismnushort  43362  ralbinrald  46129  fargshiftfva  46410  reupr  46489  evengpop3  46765  evengpoap3  46766  isomgrsym  46803  snlindsntorlem  47239