Theorem rspcv 3578

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2137, ax-11 2154, ax-12 2171. (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 22	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵)
2		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	adantl 482	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcdv 3574	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061

This theorem is referenced by:  rspccv  3579  rspcva  3580  rspccva  3581  rspcdva  3583  rspc2v  3591  rspc3v  3594  rspc4v  3596  rr19.3v  3622  rr19.28v  3623  rspsbc  3838  rspc2vd  3909  intmin  4934  ralxfrALT  5375  somo  5587  fr2nr  5616  weniso  7304  fr3nr  7711  limuni3  7793  tfinds  7801  funcnvuni  7873  poseq  8095  soseq  8096  suppfnss  8125  onnseq  8295  smo11  8315  tfrlem9  8336  tz7.49  8396  omeulem1  8534  oeordi  8539  naddelim  8637  nneneq  9160  nneneqOLD  9172  frfi  9239  unblem2  9247  unbnn2  9251  xpfiOLD  9269  ordiso2  9460  cantnflem1  9634  ttrcltr  9661  ttrclss  9665  ttrclselem2  9671  frins3  9700  rankunb  9795  tcrank  9829  carduni  9926  dfac8alem  9974  alephinit  10040  aceq3lem  10065  dfac5  10073  dfac12r  10091  dfac12k  10092  pwsdompw  10149  cflm  10195  isf32lem1  10298  isf32lem2  10299  isf34lem4  10322  hsmexlem4  10374  axcc3  10383  domtriomlem  10387  axdc3lem2  10396  axdc4lem  10400  axcclem  10402  axdclem  10464  alephval2  10517  winainflem  10638  eltskm  10788  squeeze0  12067  lbreu  12114  nnsub  12206  ublbneg  12867  zmax  12879  zbtwnre  12880  xrub  13241  infmremnf  13272  infmrp1  13273  fzrevral  13536  axdc4uzlem  13898  faclbnd4lem4  14206  ccatalpha  14493  wrdind  14622  wrd2ind  14623  reuccatpfxs1lem  14646  recan  15233  cau3lem  15251  caubnd2  15254  climrlim2  15441  climshftlem  15468  rlimcld2  15472  subcn2  15489  isercoll  15564  climcau  15567  serf0  15577  iseralt  15581  isumrpcl  15739  clim2prod  15784  ntrivcvgfvn0  15795  sqrt2irr  16142  ndvdssub  16302  dfgcd2  16438  lcmf  16520  lcmfunsnlem1  16524  lcmfunsnlem2lem1  16525  lcmfunsnlem2lem2  16526  lcmfdvdsb  16530  coprmgcdb  16536  coprmdvds1  16539  coprmprod  16548  coprmproddvdslem  16549  nprm  16575  dvdsprm  16590  coprm  16598  pcmpt  16775  pcmptdvds  16777  pcfac  16782  prmpwdvds  16787  unbenlem  16791  vdwlem10  16873  vdwlem13  16876  vdwnnlem1  16878  prmdvdsprmop  16926  prmgaplem7  16940  catideu  17569  initoid  17901  termoid  17902  initoeu1  17911  termoeu1  17918  isdrs2  18209  lublecllem  18263  lubun  18418  lidrididd  18539  sgrp2rid2ex  18751  dfgrp2  18789  grpidinv2  18820  dfgrp3lem  18859  issubg4  18961  efgi  19515  efgi2  19521  dprdss  19822  srgrz  19952  srglz  19953  srgisid  19954  f1rhm0to0ALT  20191  islmodd  20384  rmodislmod  20447  rmodislmodOLD  20448  islmhm2  20556  rrgeq0i  20796  ip2eq  21094  mvrf1  21431  cply1mul  21702  isclo2  22476  cnpnei  22652  cncls  22662  lmss  22686  cnt0  22734  isnrm2  22746  isreg2  22765  tgcmp  22789  uncmp  22791  dfconn2  22807  1stcclb  22832  2ndcctbss  22843  comppfsc  22920  kgencn2  22945  ptpjpre1  22959  txlm  23036  kqfvima  23118  kqt0lem  23124  isr0  23125  nrmr0reg  23137  fgss2  23262  isufil2  23296  cfinufil  23316  flimopn  23363  fbflim2  23365  flfneii  23380  cnpflf  23389  fclssscls  23406  fclsnei  23407  fclsrest  23412  flimfnfcls  23416  fclscmp  23418  isfcf  23422  fcfnei  23423  alexsubALTlem3  23437  alexsubALTlem4  23438  alexsubALT  23439  tsmsgsum  23527  tsmsres  23532  tsmsxplem1  23541  ustincl  23596  ustdiag  23597  ustinvel  23598  ustexhalf  23599  cfiluexsm  23679  psmet0  23698  prdsbl  23884  metss  23901  metcnp3  23933  isngp4  24005  nmoi  24129  mulc1cncf  24305  cncfco  24307  lebnumii  24366  iscfil3  24674  iscau2  24678  iscau4  24680  equivcfil  24700  equivcau  24701  lmcau  24714  ismbf  25029  ellimc3  25280  lhop1  25415  dvfsumlem4  25430  dvfsum2  25435  dgrco  25673  fta1  25705  aalioulem2  25730  aalioulem4  25732  ulmclm  25783  ulmshftlem  25785  ulmcaulem  25790  ulmcau  25791  ulmcn  25795  cxploglim  26364  ftalem3  26461  chtub  26597  dchrelbasd  26624  2sqlem6  26808  2sqlem10  26813  dchrisumlema  26873  dchrisumlem2  26875  dchrisumlem3  26876  dchrvmasumlem2  26883  pntpbnd1  26971  pntibnd  26978  pntleml  26996  nolt02o  27080  noresle  27082  nosupbnd1lem1  27093  nosupbnd1lem4  27096  nosupbnd2lem1  27100  nosupbnd2  27101  nocvxminlem  27160  madebdaylemold  27270  brbtwn2  27917  colinearalg  27922  axcontlem4  27979  usgruspgrb  28195  cusgredg  28435  cusgrres  28459  usgredgsscusgredg  28470  fusgrn0degnn0  28510  wlk1walk  28650  wlkres  28681  wlkp1lem6  28689  wlkdlem2  28694  upgrwlkdvdelem  28747  pthdlem2lem  28778  lfgrn1cycl  28813  wwlksnredwwlkn  28903  wwlksnextproplem2  28918  clwwlkccatlem  28996  clwlkclwwlkf1lem3  29013  clwwisshclwwslemlem  29020  clwwlkf1  29056  clwwlkext2edg  29063  3cyclfrgrrn1  29292  n4cyclfrgr  29298  frgrwopregasn  29323  frgrwopregbsn  29324  isgrpo  29502  blocnilem  29809  ip2eqi  29861  htthlem  29922  hial0  30107  hial02  30108  hial2eq  30111  ocorth  30296  h1de2i  30558  pjjsi  30705  lnopunilem1  31015  lnophmlem1  31021  nmcexi  31031  riesz4i  31068  mdi  31300  mdbr3  31302  mdbr4  31303  dmdi  31307  dmdbr3  31310  dmdbr4  31311  dmdi4  31312  mdslmd1i  31334  atss  31351  atom1d  31358  atmd  31404  sumdmdlem2  31424  cdj1i  31438  cdj3i  31446  fnpreimac  31654  nn0min  31786  archiabllem1a  32097  archiabllem2a  32100  archiabl  32104  isarchiofld  32183  crefi  32517  pcmplfin  32530  fmcncfil  32601  sigaclcu  32805  unelsiga  32822  sigapildsys  32850  ldgenpisys  32854  measvun  32897  carsgclctunlem2  33008  sibfima  33027  fnrelpredd  33782  pfxwlk  33804  derangenlem  33852  subfacp1lem6  33866  resconn  33927  cvmcov  33944  cvmliftlem3  33968  cvmliftphtlem  33998  satfdmfmla  34081  mclsax  34250  dfon2lem6  34449  fwddifnp1  34826  opnrebl2  34869  nn0prpwlem  34870  nn0prpw  34871  neibastop2lem  34908  neibastop2  34909  filnetlem4  34929  bj-mooreset  35646  bj-ismoored0  35650  dfgcd3  35868  fin2so  36138  poimirlem25  36176  poimirlem29  36180  poimir  36184  mbfresfi  36197  ftc1cnnclem  36222  seqpo  36279  incsequz  36280  mettrifi  36289  geomcau  36291  caushft  36293  sstotbnd2  36306  equivtotbnd  36310  totbndbnd  36321  ismtybndlem  36338  heibor1lem  36341  bfplem2  36355  opidonOLD  36384  exidu1  36388  rngoideu  36435  isdrngo2  36490  unichnidl  36563  lsat0cv  37568  lcvexchlem4  37572  lcvexchlem5  37573  eqlkr3  37636  lub0N  37724  glb0N  37728  cvrnbtwn  37806  ltrneq2  38684  trlval2  38699  lpolsatN  40024  lpolpolsatN  40025  hdmap14lem12  40415  isdomn4  40697  fsuppind  40823  nna4b4nsq  41056  incssnn0  41092  lnmlssfg  41465  unxpwdom3  41480  neik0pk1imk0  42441  ismnushort  42703  fnchoice  43356  monoordxrv  43837  monoord2xrv  43839  limcrecl  43990  fourierdlem54  44521  fourierdlem103  44570  fourierdlem104  44571  euoreqb  45461  smonoord  45683  iccpartlt  45736  iccpartgt  45739  iccpartdisj  45749  paireqne  45823  fmtnodvds  45856  perfectALTVlem2  46034  sbgoldbwt  46089  sbgoldbst  46090  sgoldbeven3prm  46095  mogoldbb  46097  nnsum4primesodd  46108  nnsum4primesoddALTV  46109  bgoldbnnsum3prm  46116  bgoldbtbndlem2  46118  bgoldbtbndlem3  46119  bgoldbtbndlem4  46120  bgoldbtbnd  46121  tgblthelfgott  46127  tgoldbach  46129  isomuspgrlem2c  46142  isomuspgrlem2d  46143  lcosslsp  46639  linindslinci  46649  lindslinindsimp1  46658  ldepsnlinclem1  46706  ldepsnlinclem2  46707  iscnrm3r  47101