Theorem rspcv 3618

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2141, ax-11 2157, ax-12 2177. (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 3614	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∀wral 3061

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062

This theorem is referenced by:  rspccv  3619  rspcva  3620  rspccva  3621  rspcdva  3623  rspc2v  3633  rspc3v  3638  rspc4v  3642  rr19.3v  3667  rr19.28v  3668  rspsbc  3879  rspc2vd  3947  intmin  4968  ralxfrALT  5415  somo  5631  fr2nr  5662  weniso  7374  fr3nr  7792  limuni3  7873  tfinds  7881  funcnvuni  7954  resf1extb  7956  poseq  8183  soseq  8184  suppfnss  8214  onnseq  8384  smo11  8404  tfrlem9  8425  tz7.49  8485  omeulem1  8620  oeordi  8625  naddelim  8724  nneneq  9246  nneneqOLD  9258  frfi  9321  unblem2  9329  unbnn2  9333  xpfiOLD  9359  ordiso2  9555  cantnflem1  9729  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  frins3  9795  rankunb  9890  tcrank  9924  carduni  10021  dfac8alem  10069  alephinit  10135  aceq3lem  10160  dfac5  10169  dfac12r  10187  dfac12k  10188  pwsdompw  10243  cflm  10290  isf32lem1  10393  isf32lem2  10394  isf34lem4  10417  hsmexlem4  10469  axcc3  10478  domtriomlem  10482  axdc3lem2  10491  axdc4lem  10495  axcclem  10497  axdclem  10559  alephval2  10612  winainflem  10733  eltskm  10883  squeeze0  12171  lbreu  12218  nnsub  12310  ublbneg  12975  zmax  12987  zbtwnre  12988  xrub  13354  infmremnf  13385  infmrp1  13386  fzrevral  13652  axdc4uzlem  14024  faclbnd4lem4  14335  ccatalpha  14631  wrdind  14760  wrd2ind  14761  reuccatpfxs1lem  14784  recan  15375  cau3lem  15393  caubnd2  15396  climrlim2  15583  climshftlem  15610  rlimcld2  15614  subcn2  15631  isercoll  15704  climcau  15707  serf0  15717  iseralt  15721  isumrpcl  15879  clim2prod  15924  ntrivcvgfvn0  15935  sqrt2irr  16285  ndvdssub  16446  dfgcd2  16583  lcmf  16670  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfdvdsb  16680  coprmgcdb  16686  coprmdvds1  16689  coprmprod  16698  coprmproddvdslem  16699  nprm  16725  dvdsprm  16740  coprm  16748  pcmpt  16930  pcmptdvds  16932  pcfac  16937  prmpwdvds  16942  unbenlem  16946  vdwlem10  17028  vdwlem13  17031  vdwnnlem1  17033  prmdvdsprmop  17081  prmgaplem7  17095  catideu  17718  initoid  18046  termoid  18047  initoeu1  18056  termoeu1  18063  isdrs2  18352  lublecllem  18405  lubun  18560  lidrididd  18683  sgrp2rid2ex  18940  dfgrp2  18980  grpidinv2  19015  dfgrp3lem  19056  issubg4  19163  efgi  19737  efgi2  19743  dprdss  20049  srgrz  20204  srglz  20205  srgisid  20206  rrgeq0i  20699  isdomn4  20716  islmodd  20864  rmodislmod  20928  islmhm2  21037  rnglidlmcl  21226  ip2eq  21671  mvrf1  22006  psdmul  22170  cply1mul  22300  isclo2  23096  cnpnei  23272  cncls  23282  lmss  23306  cnt0  23354  isnrm2  23366  isreg2  23385  tgcmp  23409  uncmp  23411  dfconn2  23427  1stcclb  23452  2ndcctbss  23463  comppfsc  23540  kgencn2  23565  ptpjpre1  23579  txlm  23656  kqfvima  23738  kqt0lem  23744  isr0  23745  nrmr0reg  23757  fgss2  23882  isufil2  23916  cfinufil  23936  flimopn  23983  fbflim2  23985  flfneii  24000  cnpflf  24009  fclssscls  24026  fclsnei  24027  fclsrest  24032  flimfnfcls  24036  fclscmp  24038  isfcf  24042  fcfnei  24043  alexsubALTlem3  24057  alexsubALTlem4  24058  alexsubALT  24059  tsmsgsum  24147  tsmsres  24152  tsmsxplem1  24161  ustincl  24216  ustdiag  24217  ustinvel  24218  ustexhalf  24219  cfiluexsm  24299  psmet0  24318  prdsbl  24504  metss  24521  metcnp3  24553  isngp4  24625  nmoi  24749  mulc1cncf  24931  cncfco  24933  lebnumii  24998  iscfil3  25307  iscau2  25311  iscau4  25313  equivcfil  25333  equivcau  25334  lmcau  25347  ismbf  25663  ellimc3  25914  lhop1  26053  dvfsumlem4  26070  dvfsum2  26075  dgrco  26315  fta1  26350  aalioulem2  26375  aalioulem4  26377  ulmclm  26430  ulmshftlem  26432  ulmcaulem  26437  ulmcau  26438  ulmcn  26442  cxploglim  27021  ftalem3  27118  chtub  27256  dchrelbasd  27283  2sqlem6  27467  2sqlem10  27472  dchrisumlema  27532  dchrisumlem2  27534  dchrisumlem3  27535  dchrvmasumlem2  27542  pntpbnd1  27630  pntibnd  27637  pntleml  27655  nolt02o  27740  noresle  27742  nosupbnd1lem1  27753  nosupbnd1lem4  27756  nosupbnd2lem1  27760  nosupbnd2  27761  nocvxminlem  27822  madebdaylemold  27936  n0subs  28360  brbtwn2  28920  colinearalg  28925  axcontlem4  28982  usgruspgrb  29200  cusgredg  29441  cusgrres  29466  usgredgsscusgredg  29477  fusgrn0degnn0  29517  wlk1walk  29657  wlkres  29688  wlkp1lem6  29696  wlkdlem2  29701  upgrwlkdvdelem  29756  pthdlem2lem  29787  lfgrn1cycl  29825  wwlksnredwwlkn  29915  wwlksnextproplem2  29930  clwwlkccatlem  30008  clwlkclwwlkf1lem3  30025  clwwisshclwwslemlem  30032  clwwlkf1  30068  clwwlkext2edg  30075  3cyclfrgrrn1  30304  n4cyclfrgr  30310  frgrwopregasn  30335  frgrwopregbsn  30336  isgrpo  30516  blocnilem  30823  ip2eqi  30875  htthlem  30936  hial0  31121  hial02  31122  hial2eq  31125  ocorth  31310  h1de2i  31572  pjjsi  31719  lnopunilem1  32029  lnophmlem1  32035  nmcexi  32045  riesz4i  32082  mdi  32314  mdbr3  32316  mdbr4  32317  dmdi  32321  dmdbr3  32324  dmdbr4  32325  dmdi4  32326  mdslmd1i  32348  atss  32365  atom1d  32372  atmd  32418  sumdmdlem2  32438  cdj1i  32452  cdj3i  32460  fnpreimac  32681  nn0min  32822  archiabllem1a  33198  archiabllem2a  33201  archiabl  33205  isarchiofld  33347  crefi  33846  pcmplfin  33859  fmcncfil  33930  sigaclcu  34118  unelsiga  34135  sigapildsys  34163  ldgenpisys  34167  measvun  34210  carsgclctunlem2  34321  sibfima  34340  fnrelpredd  35103  pfxwlk  35129  derangenlem  35176  subfacp1lem6  35190  resconn  35251  cvmcov  35268  cvmliftlem3  35292  cvmliftphtlem  35322  satfdmfmla  35405  mclsax  35574  dfon2lem6  35789  fwddifnp1  36166  opnrebl2  36322  nn0prpwlem  36323  nn0prpw  36324  neibastop2lem  36361  neibastop2  36362  filnetlem4  36382  bj-mooreset  37103  bj-ismoored0  37107  dfgcd3  37325  fin2so  37614  poimirlem25  37652  poimirlem29  37656  poimir  37660  mbfresfi  37673  ftc1cnnclem  37698  seqpo  37754  incsequz  37755  mettrifi  37764  geomcau  37766  caushft  37768  sstotbnd2  37781  equivtotbnd  37785  totbndbnd  37796  ismtybndlem  37813  heibor1lem  37816  bfplem2  37830  opidonOLD  37859  exidu1  37863  rngoideu  37910  isdrngo2  37965  unichnidl  38038  lsat0cv  39034  lcvexchlem4  39038  lcvexchlem5  39039  eqlkr3  39102  lub0N  39190  glb0N  39194  cvrnbtwn  39272  ltrneq2  40150  trlval2  40165  lpolsatN  41490  lpolpolsatN  41491  hdmap14lem12  41881  fsuppind  42600  nna4b4nsq  42670  incssnn0  42722  lnmlssfg  43092  unxpwdom3  43107  neik0pk1imk0  44060  ismnushort  44320  fnchoice  45034  monoordxrv  45492  monoord2xrv  45494  limcrecl  45644  fourierdlem54  46175  fourierdlem103  46224  fourierdlem104  46225  euoreqb  47121  smonoord  47358  iccpartlt  47411  iccpartgt  47414  iccpartdisj  47424  paireqne  47498  fmtnodvds  47531  perfectALTVlem2  47709  sbgoldbwt  47764  sbgoldbst  47765  sgoldbeven3prm  47770  mogoldbb  47772  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  bgoldbnnsum3prm  47791  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbndlem4  47795  bgoldbtbnd  47796  tgblthelfgott  47802  tgoldbach  47804  isuspgrim0  47872  grimuhgr  47878  grimcnv  47879  grimco  47880  uhgrimisgrgriclem  47898  clnbgrgrimlem  47901  clnbgrgrim  47902  grimedg  47903  uspgrlimlem3  47957  uspgrlimlem4  47958  grlimgrtrilem2  47962  grlimgrtri  47963  grilcbri2  47971  grlicsym  47973  grlictr  47975  clnbgr3stgrgrlic  47979  lcosslsp  48355  linindslinci  48365  lindslinindsimp1  48374  ldepsnlinclem1  48422  ldepsnlinclem2  48423  iscnrm3r  48845  termc2  49148