Theorem rspcv 3576

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2174, ax-11 2190, ax-12 2211. (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 485	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcdv 3572	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076

This theorem is referenced by:  rspccv  3577  rspcva  3578  rspccva  3579  rspcdva  3581  rspc2v  3591  rspc3v  3596  rspc4v  3600  rr19.3v  3625  rr19.28v  3626  rspsbc  3830  rspc2vd  3898  intmin  4923  ralxfrALT  5369  somo  5590  fr2nr  5620  weniso  7333  fr3nr  7750  limuni3  7827  tfinds  7835  funcnvuni  7908  resf1extb  7910  poseq  8132  soseq  8133  suppfnss  8163  onnseq  8309  smo11  8329  tfrlem9  8350  tz7.49  8410  omeulem1  8545  oeordi  8551  naddelim  8651  nneneq  9168  frfi  9223  unblem2  9231  unbnn2  9235  ordiso2  9457  cantnflem1  9638  ttrcltr  9665  ttrclss  9669  ttrclselem2  9675  frins3  9707  rankunb  9802  tcrank  9836  carduni  9933  dfac8alem  9979  alephinit  10045  aceq3lem  10070  dfac5  10079  dfac12r  10097  dfac12k  10098  pwsdompw  10153  cflm  10200  isf32lem1  10304  isf32lem2  10305  isf34lem4  10328  hsmexlem4  10380  axcc3  10389  domtriomlem  10393  axdc3lem2  10402  axdc4lem  10406  axcclem  10408  axdclem  10470  alephval2  10524  winainflem  10645  eltskm  10795  squeeze0  12089  lbreu  12136  nnsub  12251  ublbneg  12928  zmax  12940  zbtwnre  12941  xrub  13309  infmremnf  13341  infmrp1  13342  fzrevral  13611  axdc4uzlem  13990  faclbnd4lem4  14303  ccatalpha  14601  wrdind  14729  wrd2ind  14730  reuccatpfxs1lem  14753  recan  15355  cau3lem  15373  caubnd2  15376  climrlim2  15565  climshftlem  15592  rlimcld2  15596  subcn2  15613  isercoll  15686  climcau  15689  serf0  15699  iseralt  15703  isumrpcl  15864  clim2prod  15909  ntrivcvgfvn0  15920  sqrt2irr  16272  ndvdssub  16434  dfgcd2  16571  lcmf  16658  lcmfunsnlem1  16662  lcmfunsnlem2lem1  16663  lcmfunsnlem2lem2  16664  lcmfdvdsb  16668  coprmgcdb  16674  coprmdvds1  16677  coprmprod  16686  coprmproddvdslem  16687  nprm  16713  dvdsprm  16729  coprm  16737  pcmpt  16919  pcmptdvds  16921  pcfac  16926  prmpwdvds  16931  unbenlem  16935  vdwlem10  17017  vdwlem13  17020  vdwnnlem1  17022  prmdvdsprmop  17070  prmgaplem7  17084  catideu  17698  initoid  18025  termoid  18026  initoeu1  18035  termoeu1  18042  isdrs2  18329  lublecllem  18381  lubun  18538  lidrididd  18695  sgrp2rid2ex  18955  dfgrp2  18995  grpidinv2  19030  dfgrp3lem  19071  issubg4  19178  efgi  19750  efgi2  19756  dprdss  20062  srgrz  20244  srglz  20245  srgisid  20246  rrgeq0i  20736  isdomn4  20753  islmodd  20921  rmodislmod  20985  islmhm2  21093  rnglidlmcl  21274  ip2eq  21693  mvrf1  22025  psdmul  22219  cply1mul  22347  isclo2  23136  cnpnei  23312  cncls  23322  lmss  23346  cnt0  23394  isnrm2  23406  isreg2  23425  tgcmp  23449  uncmp  23451  dfconn2  23467  1stcclb  23492  2ndcctbss  23503  comppfsc  23580  kgencn2  23605  ptpjpre1  23619  txlm  23696  kqfvima  23778  kqt0lem  23784  isr0  23785  nrmr0reg  23797  fgss2  23922  isufil2  23956  cfinufil  23976  flimopn  24023  fbflim2  24025  flfneii  24040  cnpflf  24049  fclssscls  24066  fclsnei  24067  fclsrest  24072  flimfnfcls  24076  fclscmp  24078  isfcf  24082  fcfnei  24083  alexsubALTlem3  24097  alexsubALTlem4  24098  alexsubALT  24099  tsmsgsum  24187  tsmsres  24192  tsmsxplem1  24201  ustincl  24256  ustdiag  24257  ustinvel  24258  ustexhalf  24259  cfiluexsm  24337  psmet0  24356  prdsbl  24539  metss  24556  metcnp3  24588  isngp4  24660  nmoi  24776  mulc1cncf  24955  cncfco  24957  lebnumii  25016  iscfil3  25323  iscau2  25327  iscau4  25329  equivcfil  25349  equivcau  25350  lmcau  25363  ismbf  25678  ellimc3  25929  lhop1  26064  dvfsumlem4  26079  dvfsum2  26084  dgrco  26323  fta1  26360  aalioulem2  26385  aalioulem4  26387  ulmclm  26438  ulmshftlem  26440  ulmcaulem  26445  ulmcau  26446  ulmcn  26450  cxploglim  27030  ftalem3  27127  chtub  27264  dchrelbasd  27291  2sqlem6  27475  2sqlem10  27480  dchrisumlema  27540  dchrisumlem2  27542  dchrisumlem3  27543  dchrvmasumlem2  27550  pntpbnd1  27638  pntibnd  27645  pntleml  27663  nolt02o  27747  noresle  27749  nosupbnd1lem1  27760  nosupbnd1lem4  27763  nosupbnd2lem1  27767  nosupbnd2  27768  nocvxminlem  27835  madebdaylemold  27979  n0subs  28444  z12zsodd  28563  brbtwn2  29063  colinearalg  29068  axcontlem4  29125  usgruspgrb  29341  cusgredg  29582  cusgrres  29606  usgredgsscusgredg  29617  fusgrn0degnn0  29657  wlk1walk  29796  wlkres  29826  wlkp1lem6  29834  wlkdlem2  29839  upgrwlkdvdelem  29893  pthdlem2lem  29924  lfgrn1cycl  29962  wwlksnredwwlkn  30052  wwlksnextproplem2  30067  clwwlkccatlem  30148  clwlkclwwlkf1lem3  30165  clwwisshclwwslemlem  30172  clwwlkf1  30208  clwwlkext2edg  30215  3cyclfrgrrn1  30444  n4cyclfrgr  30450  frgrwopregasn  30475  frgrwopregbsn  30476  isgrpo  30657  blocnilem  30964  ip2eqi  31016  htthlem  31077  hial0  31262  hial02  31263  hial2eq  31266  ocorth  31451  h1de2i  31713  pjjsi  31860  lnopunilem1  32170  lnophmlem1  32176  nmcexi  32186  riesz4i  32223  mdi  32455  mdbr3  32457  mdbr4  32458  dmdi  32462  dmdbr3  32465  dmdbr4  32466  dmdi4  32467  mdslmd1i  32489  atss  32506  atom1d  32513  atmd  32559  sumdmdlem2  32579  cdj1i  32593  cdj3i  32601  fnpreimac  32833  nn0min  32984  archiabllem1a  33332  archiabllem2a  33335  archiabl  33339  isarchiofld  33340  trisecnconstr  34050  crefi  34105  pcmplfin  34118  fmcncfil  34189  sigaclcu  34375  unelsiga  34392  sigapildsys  34420  ldgenpisys  34424  measvun  34467  carsgclctunlem2  34577  sibfima  34596  fnrelpredd  35348  fineqvnttrclse  35381  fineqvinfep  35382  pfxwlk  35435  derangenlem  35482  subfacp1lem6  35496  resconn  35557  cvmcov  35574  cvmliftlem3  35598  cvmliftphtlem  35628  satfdmfmla  35711  mclsax  35880  dfon2lem6  36097  fwddifnp1  36476  opnrebl2  36642  nn0prpwlem  36643  nn0prpw  36644  neibastop2lem  36681  neibastop2  36682  filnetlem4  36702  dfttc4  36851  bj-mooreset  37553  bj-ismoored0  37557  dfgcd3  37777  fin2so  38067  poimirlem25  38105  poimirlem29  38109  poimir  38113  mbfresfi  38126  ftc1cnnclem  38151  seqpo  38207  incsequz  38208  mettrifi  38217  geomcau  38219  caushft  38221  sstotbnd2  38234  equivtotbnd  38238  totbndbnd  38249  ismtybndlem  38266  heibor1lem  38269  bfplem2  38283  opidonOLD  38312  exidu1  38316  rngoideu  38363  isdrngo2  38418  unichnidl  38491  lsat0cv  39618  lcvexchlem4  39622  lcvexchlem5  39623  eqlkr3  39686  lub0N  39774  glb0N  39778  cvrnbtwn  39856  ltrneq2  40733  trlval2  40748  lpolsatN  42073  lpolpolsatN  42074  hdmap14lem12  42464  fsuppind  43133  nna4b4nsq  43203  incssnn0  43253  lnmlssfg  43618  unxpwdom3  43633  neik0pk1imk0  44584  ismnushort  44838  fnchoice  45570  monoordxrv  46016  monoord2xrv  46018  limcrecl  46166  fourierdlem54  46695  fourierdlem103  46744  fourierdlem104  46745  euoreqb  47664  smonoord  47932  iccpartlt  47991  iccpartgt  47994  iccpartdisj  48004  paireqne  48078  fmtnodvds  48114  perfectALTVlem2  48305  sbgoldbwt  48360  sbgoldbst  48361  sgoldbeven3prm  48366  mogoldbb  48368  nnsum4primesodd  48379  nnsum4primesoddALTV  48380  bgoldbnnsum3prm  48387  bgoldbtbndlem2  48389  bgoldbtbndlem3  48390  bgoldbtbndlem4  48391  bgoldbtbnd  48392  tgblthelfgott  48398  tgoldbach  48400  grimuhgr  48470  grimcnv  48471  grimco  48472  uhgrimedgi  48473  isuspgrim0  48477  upgrimwlklem5  48484  uhgrimisgrgriclem  48513  clnbgrgrimlem  48516  clnbgrgrim  48517  grimedg  48518  uspgrlimlem3  48573  uspgrlimlem4  48574  grlimedgclnbgr  48578  grlimgrtrilem2  48585  grlimgrtri  48586  grilcbri2  48594  grlicsym  48596  grlictr  48598  clnbgr3stgrgrlim  48602  clnbgr3stgrgrlic  48603  lcosslsp  49021  linindslinci  49031  lindslinindsimp1  49040  ldepsnlinclem1  49088  ldepsnlinclem2  49089  iscnrm3r  49530  initc  49673  termc2  50100