Theorem rspcdv 3572

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081

This theorem is used by:  rspcdv2  3575  rspcv  3576  ralxfrd  5377  ralxfrd2  5381  reuop  6322  suppofss1d  8259  suppofss2d  8260  zindd  12840  wrd2ind  14914  ismri2dad  17861  mreexd  17866  mreexexlemd  17868  catcocl  17909  catass  17910  moni  17961  subccocl  18070  funcco  18096  fullfo  18139  fthf1  18144  nati  18183  chnind  18845  mndind  19074  ringurd  20462  idsrngd  21164  mpomulcn  25243  fsumdvdsmul  27579  uspgr2wlkeq  30283  crctcshwlkn0lem4  30459  crctcshwlkn0lem5  30460  wwlknllvtx  30492  0enwwlksnge1  30510  wlkiswwlks2lem5  30519  clwlkclwwlklem2a  30646  clwlkclwwlklem2  30648  clwwisshclwws  30663  clwwlkinwwlk  30688  umgr2cwwk2dif  30712  wrdt2ind  33612  mgccole1  33650  mgccole2  33651  mgcmnt1  33652  mgcmntco  33654  dfmgc2lem  33655  1arithufdlem3  34182  dfufd2  34186  fedgmullem2  34373  constrconj  34488  zart0  34622  zarcmplem  34624  esumcvg  34829  inelcarsg  35054  carsgclctunlem1  35060  orvcelel  35213  signsply0  35291  onint1  37452  qsalrel  43559  ismnushort  45546  ralbinrald  48466  fargshiftfva  48798  reupr  48877  evengpop3  49169  evengpoap3  49170  snlindsntorlem  49913