Theorem rspcdv 3577

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rspcdv2  3580  rspcv  3581  ralxfrd  5358  ralxfrd2  5362  reuop  6254  suppofss1d  8160  suppofss2d  8161  zindd  12611  wrd2ind  14664  ismri2dad  17574  mreexd  17579  mreexexlemd  17581  catcocl  17622  catass  17623  moni  17674  subccocl  17783  funcco  17809  fullfo  17852  fthf1  17857  nati  17896  mndind  18731  ringurd  20070  idsrngd  20741  mpomulcn  24734  fsumdvdsmul  27081  uspgr2wlkeq  29549  crctcshwlkn0lem4  29716  crctcshwlkn0lem5  29717  wwlknllvtx  29749  0enwwlksnge1  29767  wlkiswwlks2lem5  29776  clwlkclwwlklem2a  29900  clwlkclwwlklem2  29902  clwwisshclwws  29917  clwwlkinwwlk  29942  umgr2cwwk2dif  29966  wrdt2ind  32848  mgccole1  32889  mgccole2  32890  mgcmnt1  32891  mgcmntco  32893  dfmgc2lem  32894  chnind  32910  1arithufdlem3  33490  dfufd2  33494  fedgmullem2  33599  constrconj  33708  zart0  33842  zarcmplem  33844  esumcvg  34049  inelcarsg  34275  carsgclctunlem1  34281  orvcelel  34434  signsply0  34515  onint1  36410  qsalrel  42201  ismnushort  44263  ralbinrald  47096  fargshiftfva  47417  reupr  47496  evengpop3  47772  evengpoap3  47773  snlindsntorlem  48432