Theorem rspcv 3586

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2182, ax-11 2198, ax-12 2219. (Revised by SN, 12-Dec-2023.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcv	⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcv

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵)
2		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	adantl 486	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcdv 3582	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086

This theorem is referenced by:  rspccv  3587  rspcva  3588  rspccva  3589  rspcdva  3591  rspc2v  3601  rspc3v  3606  rspc4v  3610  rr19.3v  3635  rr19.28v  3636  rspsbc  3841  rspc2vd  3909  intmin  4934  ralxfrALT  5384  somo  5606  fr2nr  5636  weniso  7350  fr3nr  7767  limuni3  7844  tfinds  7852  funcnvuni  7925  resf1extb  7927  poseq  8150  soseq  8151  suppfnss  8181  onnseq  8327  smo11  8347  tfrlem9  8368  tz7.49  8428  omeulem1  8563  oeordi  8569  naddelim  8669  nneneq  9186  frfi  9241  unblem2  9249  unbnn2  9253  ordiso2  9473  cantnflem1  9654  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  frins3  9723  rankunb  9818  tcrank  9852  carduni  9963  dfac8alem  10009  alephinit  10075  aceq3lem  10100  dfac5  10108  dfac12r  10126  dfac12k  10127  pwsdompw  10182  cflm  10229  isf32lem1  10333  isf32lem2  10334  isf34lem4  10357  hsmexlem4  10409  axcc3  10418  domtriomlem  10422  axdc3lem2  10431  axdc4lem  10435  axcclem  10437  axdclem  10499  alephval2  10553  winainflem  10674  eltskm  10824  squeeze0  12114  lbreu  12161  nnsub  12276  ublbneg  12953  zmax  12965  zbtwnre  12966  xrub  13334  infmremnf  13366  infmrp1  13367  fzrevral  13636  axdc4uzlem  14015  faclbnd4lem4  14328  ccatalpha  14627  wrdind  14755  wrd2ind  14756  reuccatpfxs1lem  14779  recan  15384  cau3lem  15402  caubnd2  15405  climrlim2  15594  climshftlem  15621  rlimcld2  15625  subcn2  15642  isercoll  15715  climcau  15718  serf0  15728  iseralt  15732  isumrpcl  15893  clim2prod  15938  ntrivcvgfvn0  15949  sqrt2irr  16301  ndvdssub  16463  dfgcd2  16600  lcmf  16687  lcmfunsnlem1  16691  lcmfunsnlem2lem1  16692  lcmfunsnlem2lem2  16693  lcmfdvdsb  16697  coprmgcdb  16703  coprmdvds1  16706  coprmprod  16715  coprmproddvdslem  16716  nprm  16742  dvdsprm  16758  coprm  16766  pcmpt  16948  pcmptdvds  16950  pcfac  16955  prmpwdvds  16960  unbenlem  16964  vdwlem10  17046  vdwlem13  17049  vdwnnlem1  17051  prmdvdsprmop  17099  prmgaplem7  17113  catideu  17727  initoid  18054  termoid  18055  initoeu1  18064  termoeu1  18071  isdrs2  18358  lublecllem  18410  lubun  18567  lidrididd  18724  sgrp2rid2ex  18985  dfgrp2  19025  grpidinv2  19060  dfgrp3lem  19100  issubg4  19208  efgi  19785  efgi2  19791  dprdss  20097  srgrz  20285  srglz  20286  srgisid  20287  rrgeq0i  20780  isdomn4  20796  islmodd  20961  rmodislmod  21025  islmhm2  21133  rnglidlmcl  21315  ip2eq  21768  mvrf1  22100  psdmul  22294  cply1mul  22421  isclo2  23210  cnpnei  23386  cncls  23396  lmss  23420  cnt0  23468  isnrm2  23480  isreg2  23499  tgcmp  23523  uncmp  23525  dfconn2  23541  1stcclb  23566  2ndcctbss  23577  comppfsc  23654  kgencn2  23679  ptpjpre1  23693  txlm  23770  kqfvima  23852  kqt0lem  23858  isr0  23859  nrmr0reg  23871  fgss2  23996  isufil2  24030  cfinufil  24050  flimopn  24097  fbflim2  24099  flfneii  24114  cnpflf  24123  fclssscls  24140  fclsnei  24141  fclsrest  24146  flimfnfcls  24150  fclscmp  24152  isfcf  24156  fcfnei  24157  alexsubALTlem3  24171  alexsubALTlem4  24172  alexsubALT  24173  tsmsgsum  24261  tsmsres  24266  tsmsxplem1  24275  ustincl  24330  ustdiag  24331  ustinvel  24332  ustexhalf  24333  cfiluexsm  24411  psmet0  24430  prdsbl  24613  metss  24630  metcnp3  24662  isngp4  24734  nmoi  24850  mulc1cncf  25029  cncfco  25031  lebnumii  25090  iscfil3  25397  iscau2  25401  iscau4  25403  equivcfil  25423  equivcau  25424  lmcau  25437  ismbf  25752  ellimc3  26003  lhop1  26138  dvfsumlem4  26153  dvfsum2  26158  dgrco  26397  fta1  26434  aalioulem2  26459  aalioulem4  26461  ulmclm  26512  ulmshftlem  26514  ulmcaulem  26519  ulmcau  26520  ulmcn  26524  cxploglim  27104  ftalem3  27201  chtub  27338  dchrelbasd  27365  2sqlem6  27549  2sqlem10  27554  dchrisumlema  27614  dchrisumlem2  27616  dchrisumlem3  27617  dchrvmasumlem2  27624  pntpbnd1  27712  pntibnd  27719  pntleml  27737  nolt02o  27821  noresle  27823  nosupbnd1lem1  27834  nosupbnd1lem4  27837  nosupbnd2lem1  27841  nosupbnd2  27842  nocvxminlem  27909  madebdaylemold  28053  n0subs  28518  z12zsodd  28637  brbtwn2  29192  colinearalg  29197  axcontlem4  29254  usgruspgrb  29470  cusgredg  29711  cusgrres  29735  usgredgsscusgredg  29746  fusgrn0degnn0  29786  wlk1walk  29925  wlkres  29955  wlkp1lem6  29963  wlkdlem2  29968  upgrwlkdvdelem  30022  pthdlem2lem  30053  lfgrn1cycl  30091  wwlksnredwwlkn  30181  wwlksnextproplem2  30196  clwwlkccatlem  30277  clwlkclwwlkf1lem3  30294  clwwisshclwwslemlem  30301  clwwlkf1  30337  clwwlkext2edg  30344  3cyclfrgrrn1  30573  n4cyclfrgr  30579  frgrwopregasn  30604  frgrwopregbsn  30605  isgrpo  30786  blocnilem  31093  ip2eqi  31145  htthlem  31206  hial0  31391  hial02  31392  hial2eq  31395  ocorth  31580  h1de2i  31842  pjjsi  31989  lnopunilem1  32299  lnophmlem1  32305  nmcexi  32315  riesz4i  32352  mdi  32584  mdbr3  32586  mdbr4  32587  dmdi  32591  dmdbr3  32594  dmdbr4  32595  dmdi4  32596  mdslmd1i  32618  atss  32635  atom1d  32642  atmd  32688  sumdmdlem2  32708  cdj1i  32722  cdj3i  32730  fnpreimac  32952  nn0min  33102  archiabllem1a  33448  archiabllem2a  33451  archiabl  33455  isarchiofld  33456  trisecnconstr  34123  crefi  34178  pcmplfin  34191  fmcncfil  34262  sigaclcu  34448  unelsiga  34465  sigapildsys  34493  ldgenpisys  34497  measvun  34540  carsgclctunlem2  34650  sibfima  34669  fnrelpredd  35421  fineqvnttrclse  35456  fineqvinfep  35457  pfxwlk  35511  derangenlem  35558  subfacp1lem6  35572  resconn  35633  cvmcov  35650  cvmliftlem3  35674  cvmliftphtlem  35704  satfdmfmla  35787  mclsax  35956  dfon2lem6  36173  fwddifnp1  36552  opnrebl2  36717  nn0prpwlem  36718  nn0prpw  36719  neibastop2lem  36756  neibastop2  36757  filnetlem4  36777  dfttc4  36926  bj-mooreset  37627  bj-ismoored0  37631  dfgcd3  37851  fin2so  38141  poimirlem25  38179  poimirlem29  38183  poimir  38187  mbfresfi  38200  ftc1cnnclem  38225  seqpo  38281  incsequz  38282  mettrifi  38291  geomcau  38293  caushft  38295  sstotbnd2  38308  equivtotbnd  38312  totbndbnd  38323  ismtybndlem  38340  heibor1lem  38343  bfplem2  38357  opidonOLD  38386  exidu1  38390  rngoideu  38437  isdrngo2  38492  unichnidl  38565  lsat0cv  39692  lcvexchlem4  39696  lcvexchlem5  39697  eqlkr3  39760  lub0N  39848  glb0N  39852  cvrnbtwn  39930  ltrneq2  40807  trlval2  40822  lpolsatN  42147  lpolpolsatN  42148  hdmap14lem12  42538  fsuppind  43209  nna4b4nsq  43279  incssnn0  43329  lnmlssfg  43694  unxpwdom3  43709  neik0pk1imk0  44660  ismnushort  44898  fnchoice  45636  monoordxrv  46082  monoord2xrv  46084  limcrecl  46232  fourierdlem54  46761  fourierdlem103  46810  fourierdlem104  46811  euoreqb  47730  smonoord  47998  iccpartlt  48057  iccpartgt  48060  iccpartdisj  48070  paireqne  48144  fmtnodvds  48180  perfectALTVlem2  48371  sbgoldbwt  48426  sbgoldbst  48427  sgoldbeven3prm  48432  mogoldbb  48434  nnsum4primesodd  48445  nnsum4primesoddALTV  48446  bgoldbnnsum3prm  48453  bgoldbtbndlem2  48455  bgoldbtbndlem3  48456  bgoldbtbndlem4  48457  bgoldbtbnd  48458  tgblthelfgott  48464  tgoldbach  48466  grimuhgr  48536  grimcnv  48537  grimco  48538  uhgrimedgi  48539  isuspgrim0  48543  upgrimwlklem5  48550  uhgrimisgrgriclem  48579  clnbgrgrimlem  48582  clnbgrgrim  48583  grimedg  48584  uspgrlimlem3  48639  uspgrlimlem4  48640  grlimedgclnbgr  48644  grlimgrtrilem2  48651  grlimgrtri  48652  grilcbri2  48660  grlicsym  48662  grlictr  48664  clnbgr3stgrgrlim  48668  clnbgr3stgrgrlic  48669  lcosslsp  49098  linindslinci  49108  lindslinindsimp1  49117  ldepsnlinclem1  49165  ldepsnlinclem2  49166  iscnrm3r  49606  initc  49749  termc2  50176