Theorem rspcv 3569

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049

This theorem is referenced by:  rspccv  3570  rspcva  3571  rspccva  3572  rspcdva  3574  rspc2v  3584  rspc3v  3589  rspc4v  3593  rr19.3v  3618  rr19.28v  3619  rspsbc  3826  rspc2vd  3894  intmin  4920  ralxfrALT  5357  somo  5568  fr2nr  5598  weniso  7297  fr3nr  7714  limuni3  7791  tfinds  7799  funcnvuni  7871  resf1extb  7873  poseq  8097  soseq  8098  suppfnss  8128  onnseq  8273  smo11  8293  tfrlem9  8313  tz7.49  8373  omeulem1  8506  oeordi  8511  naddelim  8610  nneneq  9126  frfi  9180  unblem2  9188  unbnn2  9192  ordiso2  9412  cantnflem1  9590  ttrcltr  9617  ttrclss  9621  ttrclselem2  9627  frins3  9659  rankunb  9754  tcrank  9788  carduni  9885  dfac8alem  9931  alephinit  9997  aceq3lem  10022  dfac5  10031  dfac12r  10049  dfac12k  10050  pwsdompw  10105  cflm  10152  isf32lem1  10255  isf32lem2  10256  isf34lem4  10279  hsmexlem4  10331  axcc3  10340  domtriomlem  10344  axdc3lem2  10353  axdc4lem  10357  axcclem  10359  axdclem  10421  alephval2  10474  winainflem  10595  eltskm  10745  squeeze0  12036  lbreu  12083  nnsub  12180  ublbneg  12837  zmax  12849  zbtwnre  12850  xrub  13218  infmremnf  13250  infmrp1  13251  fzrevral  13519  axdc4uzlem  13897  faclbnd4lem4  14210  ccatalpha  14508  wrdind  14636  wrd2ind  14637  reuccatpfxs1lem  14660  recan  15251  cau3lem  15269  caubnd2  15272  climrlim2  15461  climshftlem  15488  rlimcld2  15492  subcn2  15509  isercoll  15582  climcau  15585  serf0  15595  iseralt  15599  isumrpcl  15757  clim2prod  15802  ntrivcvgfvn0  15813  sqrt2irr  16165  ndvdssub  16327  dfgcd2  16464  lcmf  16551  lcmfunsnlem1  16555  lcmfunsnlem2lem1  16556  lcmfunsnlem2lem2  16557  lcmfdvdsb  16561  coprmgcdb  16567  coprmdvds1  16570  coprmprod  16579  coprmproddvdslem  16580  nprm  16606  dvdsprm  16621  coprm  16629  pcmpt  16811  pcmptdvds  16813  pcfac  16818  prmpwdvds  16823  unbenlem  16827  vdwlem10  16909  vdwlem13  16912  vdwnnlem1  16914  prmdvdsprmop  16962  prmgaplem7  16976  catideu  17589  initoid  17916  termoid  17917  initoeu1  17926  termoeu1  17933  isdrs2  18220  lublecllem  18272  lubun  18429  lidrididd  18586  sgrp2rid2ex  18843  dfgrp2  18883  grpidinv2  18918  dfgrp3lem  18959  issubg4  19066  efgi  19639  efgi2  19645  dprdss  19951  srgrz  20133  srglz  20134  srgisid  20135  rrgeq0i  20623  isdomn4  20640  islmodd  20808  rmodislmod  20872  islmhm2  20981  rnglidlmcl  21162  ip2eq  21599  mvrf1  21932  psdmul  22100  cply1mul  22231  isclo2  23023  cnpnei  23199  cncls  23209  lmss  23233  cnt0  23281  isnrm2  23293  isreg2  23312  tgcmp  23336  uncmp  23338  dfconn2  23354  1stcclb  23379  2ndcctbss  23390  comppfsc  23467  kgencn2  23492  ptpjpre1  23506  txlm  23583  kqfvima  23665  kqt0lem  23671  isr0  23672  nrmr0reg  23684  fgss2  23809  isufil2  23843  cfinufil  23863  flimopn  23910  fbflim2  23912  flfneii  23927  cnpflf  23936  fclssscls  23953  fclsnei  23954  fclsrest  23959  flimfnfcls  23963  fclscmp  23965  isfcf  23969  fcfnei  23970  alexsubALTlem3  23984  alexsubALTlem4  23985  alexsubALT  23986  tsmsgsum  24074  tsmsres  24079  tsmsxplem1  24088  ustincl  24143  ustdiag  24144  ustinvel  24145  ustexhalf  24146  cfiluexsm  24224  psmet0  24243  prdsbl  24426  metss  24443  metcnp3  24475  isngp4  24547  nmoi  24663  mulc1cncf  24845  cncfco  24847  lebnumii  24912  iscfil3  25220  iscau2  25224  iscau4  25226  equivcfil  25246  equivcau  25247  lmcau  25260  ismbf  25576  ellimc3  25827  lhop1  25966  dvfsumlem4  25983  dvfsum2  25988  dgrco  26228  fta1  26263  aalioulem2  26288  aalioulem4  26290  ulmclm  26343  ulmshftlem  26345  ulmcaulem  26350  ulmcau  26351  ulmcn  26355  cxploglim  26935  ftalem3  27032  chtub  27170  dchrelbasd  27197  2sqlem6  27381  2sqlem10  27386  dchrisumlema  27446  dchrisumlem2  27448  dchrisumlem3  27449  dchrvmasumlem2  27456  pntpbnd1  27544  pntibnd  27551  pntleml  27569  nolt02o  27654  noresle  27656  nosupbnd1lem1  27667  nosupbnd1lem4  27670  nosupbnd2lem1  27674  nosupbnd2  27675  nocvxminlem  27737  madebdaylemold  27863  n0subs  28309  zs12zodd  28412  brbtwn2  28904  colinearalg  28909  axcontlem4  28966  usgruspgrb  29182  cusgredg  29423  cusgrres  29448  usgredgsscusgredg  29459  fusgrn0degnn0  29499  wlk1walk  29638  wlkres  29668  wlkp1lem6  29676  wlkdlem2  29681  upgrwlkdvdelem  29735  pthdlem2lem  29766  lfgrn1cycl  29804  wwlksnredwwlkn  29894  wwlksnextproplem2  29909  clwwlkccatlem  29990  clwlkclwwlkf1lem3  30007  clwwisshclwwslemlem  30014  clwwlkf1  30050  clwwlkext2edg  30057  3cyclfrgrrn1  30286  n4cyclfrgr  30292  frgrwopregasn  30317  frgrwopregbsn  30318  isgrpo  30498  blocnilem  30805  ip2eqi  30857  htthlem  30918  hial0  31103  hial02  31104  hial2eq  31107  ocorth  31292  h1de2i  31554  pjjsi  31701  lnopunilem1  32011  lnophmlem1  32017  nmcexi  32027  riesz4i  32064  mdi  32296  mdbr3  32298  mdbr4  32299  dmdi  32303  dmdbr3  32306  dmdbr4  32307  dmdi4  32308  mdslmd1i  32330  atss  32347  atom1d  32354  atmd  32400  sumdmdlem2  32420  cdj1i  32434  cdj3i  32442  fnpreimac  32675  nn0min  32829  archiabllem1a  33201  archiabllem2a  33204  archiabl  33208  isarchiofld  33209  trisecnconstr  33877  crefi  33932  pcmplfin  33945  fmcncfil  34016  sigaclcu  34202  unelsiga  34219  sigapildsys  34247  ldgenpisys  34251  measvun  34294  carsgclctunlem2  34404  sibfima  34423  fnrelpredd  35174  fineqvnttrclse  35216  pfxwlk  35240  derangenlem  35287  subfacp1lem6  35301  resconn  35362  cvmcov  35379  cvmliftlem3  35403  cvmliftphtlem  35433  satfdmfmla  35516  mclsax  35685  dfon2lem6  35902  fwddifnp1  36281  opnrebl2  36437  nn0prpwlem  36438  nn0prpw  36439  neibastop2lem  36476  neibastop2  36477  filnetlem4  36497  bj-mooreset  37219  bj-ismoored0  37223  dfgcd3  37441  fin2so  37720  poimirlem25  37758  poimirlem29  37762  poimir  37766  mbfresfi  37779  ftc1cnnclem  37804  seqpo  37860  incsequz  37861  mettrifi  37870  geomcau  37872  caushft  37874  sstotbnd2  37887  equivtotbnd  37891  totbndbnd  37902  ismtybndlem  37919  heibor1lem  37922  bfplem2  37936  opidonOLD  37965  exidu1  37969  rngoideu  38016  isdrngo2  38071  unichnidl  38144  lsat0cv  39205  lcvexchlem4  39209  lcvexchlem5  39210  eqlkr3  39273  lub0N  39361  glb0N  39365  cvrnbtwn  39443  ltrneq2  40320  trlval2  40335  lpolsatN  41660  lpolpolsatN  41661  hdmap14lem12  42051  fsuppind  42748  nna4b4nsq  42818  incssnn0  42868  lnmlssfg  43237  unxpwdom3  43252  neik0pk1imk0  44204  ismnushort  44458  fnchoice  45190  monoordxrv  45641  monoord2xrv  45643  limcrecl  45791  fourierdlem54  46320  fourierdlem103  46369  fourierdlem104  46370  euoreqb  47271  smonoord  47533  iccpartlt  47586  iccpartgt  47589  iccpartdisj  47599  paireqne  47673  fmtnodvds  47706  perfectALTVlem2  47884  sbgoldbwt  47939  sbgoldbst  47940  sgoldbeven3prm  47945  mogoldbb  47947  nnsum4primesodd  47958  nnsum4primesoddALTV  47959  bgoldbnnsum3prm  47966  bgoldbtbndlem2  47968  bgoldbtbndlem3  47969  bgoldbtbndlem4  47970  bgoldbtbnd  47971  tgblthelfgott  47977  tgoldbach  47979  grimuhgr  48049  grimcnv  48050  grimco  48051  uhgrimedgi  48052  isuspgrim0  48056  upgrimwlklem5  48063  uhgrimisgrgriclem  48092  clnbgrgrimlem  48095  clnbgrgrim  48096  grimedg  48097  uspgrlimlem3  48152  uspgrlimlem4  48153  grlimedgclnbgr  48157  grlimgrtrilem2  48164  grlimgrtri  48165  grilcbri2  48173  grlicsym  48175  grlictr  48177  clnbgr3stgrgrlim  48181  clnbgr3stgrgrlic  48182  lcosslsp  48600  linindslinci  48610  lindslinindsimp1  48619  ldepsnlinclem1  48667  ldepsnlinclem2  48668  iscnrm3r  49109  initc  49252  termc2  49679