Theorem rspcdv 3543

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068

This theorem is referenced by:  rspcdv2  3546  rspcv  3547  ralxfrd  5326  ralxfrd2  5330  reuop  6185  suppofss1d  7991  suppofss2d  7992  zindd  12351  wrd2ind  14364  ismri2dad  17263  mreexd  17268  mreexexlemd  17270  catcocl  17311  catass  17312  moni  17365  subccocl  17476  funcco  17502  fullfo  17544  fthf1  17549  nati  17587  mndind  18381  idsrngd  20037  uspgr2wlkeq  27915  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  wwlknllvtx  28112  0enwwlksnge1  28130  wlkiswwlks2lem5  28139  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwwisshclwws  28280  clwwlkinwwlk  28305  umgr2cwwk2dif  28329  wrdt2ind  31127  mgccole1  31170  mgccole2  31171  mgcmnt1  31172  mgcmntco  31174  dfmgc2lem  31175  rngurd  31384  fedgmullem2  31613  zart0  31731  zarcmplem  31733  esumcvg  31954  inelcarsg  32178  carsgclctunlem1  32184  orvcelel  32336  signsply0  32430  onint1  34565  qsalrel  40141  ismnushort  41808  ralbinrald  44501  fargshiftfva  44783  reupr  44862  evengpop3  45138  evengpoap3  45139  isomgrsym  45176  snlindsntorlem  45699