Theorem rspcdv 3568

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  rspcdv2  3571  rspcv  3572  ralxfrd  5369  ralxfrd2  5373  reuop  6298  suppofss1d  8226  suppofss2d  8227  zindd  12805  wrd2ind  14878  ismri2dad  17818  mreexd  17823  mreexexlemd  17825  catcocl  17866  catass  17867  moni  17918  subccocl  18027  funcco  18053  fullfo  18096  fthf1  18101  nati  18140  chnind  18802  mndind  19031  ringurd  20418  idsrngd  21120  mpomulcn  25195  fsumdvdsmul  27529  uspgr2wlkeq  30233  crctcshwlkn0lem4  30409  crctcshwlkn0lem5  30410  wwlknllvtx  30442  0enwwlksnge1  30460  wlkiswwlks2lem5  30469  clwlkclwwlklem2a  30596  clwlkclwwlklem2  30598  clwwisshclwws  30613  clwwlkinwwlk  30638  umgr2cwwk2dif  30662  wrdt2ind  33564  mgccole1  33599  mgccole2  33600  mgcmnt1  33601  mgcmntco  33603  dfmgc2lem  33604  1arithufdlem3  34126  dfufd2  34130  fedgmullem2  34310  constrconj  34425  zart0  34559  zarcmplem  34561  esumcvg  34766  inelcarsg  34991  carsgclctunlem1  34997  orvcelel  35150  signsply0  35228  onint1  37331  qsalrel  43399  ismnushort  45392  ralbinrald  48299  fargshiftfva  48632  reupr  48711  evengpop3  49003  evengpoap3  49004  snlindsntorlem  49689