Theorem rspcv 3573

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rspccv  3574  rspcva  3575  rspccva  3576  rspcdva  3578  rspc2v  3588  rspc3v  3593  rspc4v  3597  rr19.3v  3622  rr19.28v  3623  rspsbc  3831  rspc2vd  3899  intmin  4918  ralxfrALT  5354  somo  5566  fr2nr  5596  weniso  7291  fr3nr  7708  limuni3  7785  tfinds  7793  funcnvuni  7865  resf1extb  7867  poseq  8091  soseq  8092  suppfnss  8122  onnseq  8267  smo11  8287  tfrlem9  8307  tz7.49  8367  omeulem1  8500  oeordi  8505  naddelim  8604  nneneq  9120  frfi  9174  unblem2  9182  unbnn2  9186  ordiso2  9407  cantnflem1  9585  ttrcltr  9612  ttrclss  9616  ttrclselem2  9622  frins3  9651  rankunb  9746  tcrank  9780  carduni  9877  dfac8alem  9923  alephinit  9989  aceq3lem  10014  dfac5  10023  dfac12r  10041  dfac12k  10042  pwsdompw  10097  cflm  10144  isf32lem1  10247  isf32lem2  10248  isf34lem4  10271  hsmexlem4  10323  axcc3  10332  domtriomlem  10336  axdc3lem2  10345  axdc4lem  10349  axcclem  10351  axdclem  10413  alephval2  10466  winainflem  10587  eltskm  10737  squeeze0  12028  lbreu  12075  nnsub  12172  ublbneg  12834  zmax  12846  zbtwnre  12847  xrub  13214  infmremnf  13246  infmrp1  13247  fzrevral  13515  axdc4uzlem  13890  faclbnd4lem4  14203  ccatalpha  14500  wrdind  14628  wrd2ind  14629  reuccatpfxs1lem  14652  recan  15244  cau3lem  15262  caubnd2  15265  climrlim2  15454  climshftlem  15481  rlimcld2  15485  subcn2  15502  isercoll  15575  climcau  15578  serf0  15588  iseralt  15592  isumrpcl  15750  clim2prod  15795  ntrivcvgfvn0  15806  sqrt2irr  16158  ndvdssub  16320  dfgcd2  16457  lcmf  16544  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfdvdsb  16554  coprmgcdb  16560  coprmdvds1  16563  coprmprod  16572  coprmproddvdslem  16573  nprm  16599  dvdsprm  16614  coprm  16622  pcmpt  16804  pcmptdvds  16806  pcfac  16811  prmpwdvds  16816  unbenlem  16820  vdwlem10  16902  vdwlem13  16905  vdwnnlem1  16907  prmdvdsprmop  16955  prmgaplem7  16969  catideu  17581  initoid  17908  termoid  17909  initoeu1  17918  termoeu1  17925  isdrs2  18212  lublecllem  18264  lubun  18421  lidrididd  18544  sgrp2rid2ex  18801  dfgrp2  18841  grpidinv2  18876  dfgrp3lem  18917  issubg4  19024  efgi  19598  efgi2  19604  dprdss  19910  srgrz  20092  srglz  20093  srgisid  20094  rrgeq0i  20584  isdomn4  20601  islmodd  20769  rmodislmod  20833  islmhm2  20942  rnglidlmcl  21123  ip2eq  21560  mvrf1  21893  psdmul  22051  cply1mul  22181  isclo2  22973  cnpnei  23149  cncls  23159  lmss  23183  cnt0  23231  isnrm2  23243  isreg2  23262  tgcmp  23286  uncmp  23288  dfconn2  23304  1stcclb  23329  2ndcctbss  23340  comppfsc  23417  kgencn2  23442  ptpjpre1  23456  txlm  23533  kqfvima  23615  kqt0lem  23621  isr0  23622  nrmr0reg  23634  fgss2  23759  isufil2  23793  cfinufil  23813  flimopn  23860  fbflim2  23862  flfneii  23877  cnpflf  23886  fclssscls  23903  fclsnei  23904  fclsrest  23909  flimfnfcls  23913  fclscmp  23915  isfcf  23919  fcfnei  23920  alexsubALTlem3  23934  alexsubALTlem4  23935  alexsubALT  23936  tsmsgsum  24024  tsmsres  24029  tsmsxplem1  24038  ustincl  24093  ustdiag  24094  ustinvel  24095  ustexhalf  24096  cfiluexsm  24175  psmet0  24194  prdsbl  24377  metss  24394  metcnp3  24426  isngp4  24498  nmoi  24614  mulc1cncf  24796  cncfco  24798  lebnumii  24863  iscfil3  25171  iscau2  25175  iscau4  25177  equivcfil  25197  equivcau  25198  lmcau  25211  ismbf  25527  ellimc3  25778  lhop1  25917  dvfsumlem4  25934  dvfsum2  25939  dgrco  26179  fta1  26214  aalioulem2  26239  aalioulem4  26241  ulmclm  26294  ulmshftlem  26296  ulmcaulem  26301  ulmcau  26302  ulmcn  26306  cxploglim  26886  ftalem3  26983  chtub  27121  dchrelbasd  27148  2sqlem6  27332  2sqlem10  27337  dchrisumlema  27397  dchrisumlem2  27399  dchrisumlem3  27400  dchrvmasumlem2  27407  pntpbnd1  27495  pntibnd  27502  pntleml  27520  nolt02o  27605  noresle  27607  nosupbnd1lem1  27618  nosupbnd1lem4  27621  nosupbnd2lem1  27625  nosupbnd2  27626  nocvxminlem  27688  madebdaylemold  27812  n0subs  28258  zs12zodd  28359  brbtwn2  28850  colinearalg  28855  axcontlem4  28912  usgruspgrb  29128  cusgredg  29369  cusgrres  29394  usgredgsscusgredg  29405  fusgrn0degnn0  29445  wlk1walk  29584  wlkres  29614  wlkp1lem6  29622  wlkdlem2  29627  upgrwlkdvdelem  29681  pthdlem2lem  29712  lfgrn1cycl  29750  wwlksnredwwlkn  29840  wwlksnextproplem2  29855  clwwlkccatlem  29933  clwlkclwwlkf1lem3  29950  clwwisshclwwslemlem  29957  clwwlkf1  29993  clwwlkext2edg  30000  3cyclfrgrrn1  30229  n4cyclfrgr  30235  frgrwopregasn  30260  frgrwopregbsn  30261  isgrpo  30441  blocnilem  30748  ip2eqi  30800  htthlem  30861  hial0  31046  hial02  31047  hial2eq  31050  ocorth  31235  h1de2i  31497  pjjsi  31644  lnopunilem1  31954  lnophmlem1  31960  nmcexi  31970  riesz4i  32007  mdi  32239  mdbr3  32241  mdbr4  32242  dmdi  32246  dmdbr3  32249  dmdbr4  32250  dmdi4  32251  mdslmd1i  32273  atss  32290  atom1d  32297  atmd  32343  sumdmdlem2  32363  cdj1i  32377  cdj3i  32385  fnpreimac  32614  nn0min  32765  archiabllem1a  33133  archiabllem2a  33136  archiabl  33140  isarchiofld  33141  trisecnconstr  33759  crefi  33814  pcmplfin  33827  fmcncfil  33898  sigaclcu  34084  unelsiga  34101  sigapildsys  34129  ldgenpisys  34133  measvun  34176  carsgclctunlem2  34287  sibfima  34306  fnrelpredd  35056  pfxwlk  35097  derangenlem  35144  subfacp1lem6  35158  resconn  35219  cvmcov  35236  cvmliftlem3  35260  cvmliftphtlem  35290  satfdmfmla  35373  mclsax  35542  dfon2lem6  35762  fwddifnp1  36139  opnrebl2  36295  nn0prpwlem  36296  nn0prpw  36297  neibastop2lem  36334  neibastop2  36335  filnetlem4  36355  bj-mooreset  37076  bj-ismoored0  37080  dfgcd3  37298  fin2so  37587  poimirlem25  37625  poimirlem29  37629  poimir  37633  mbfresfi  37646  ftc1cnnclem  37671  seqpo  37727  incsequz  37728  mettrifi  37737  geomcau  37739  caushft  37741  sstotbnd2  37754  equivtotbnd  37758  totbndbnd  37769  ismtybndlem  37786  heibor1lem  37789  bfplem2  37803  opidonOLD  37832  exidu1  37836  rngoideu  37883  isdrngo2  37938  unichnidl  38011  lsat0cv  39012  lcvexchlem4  39016  lcvexchlem5  39017  eqlkr3  39080  lub0N  39168  glb0N  39172  cvrnbtwn  39250  ltrneq2  40127  trlval2  40142  lpolsatN  41467  lpolpolsatN  41468  hdmap14lem12  41858  fsuppind  42563  nna4b4nsq  42633  incssnn0  42684  lnmlssfg  43053  unxpwdom3  43068  neik0pk1imk0  44020  ismnushort  44274  fnchoice  45007  monoordxrv  45460  monoord2xrv  45462  limcrecl  45610  fourierdlem54  46141  fourierdlem103  46190  fourierdlem104  46191  euoreqb  47093  smonoord  47355  iccpartlt  47408  iccpartgt  47411  iccpartdisj  47421  paireqne  47495  fmtnodvds  47528  perfectALTVlem2  47706  sbgoldbwt  47761  sbgoldbst  47762  sgoldbeven3prm  47767  mogoldbb  47769  nnsum4primesodd  47780  nnsum4primesoddALTV  47781  bgoldbnnsum3prm  47788  bgoldbtbndlem2  47790  bgoldbtbndlem3  47791  bgoldbtbndlem4  47792  bgoldbtbnd  47793  tgblthelfgott  47799  tgoldbach  47801  grimuhgr  47871  grimcnv  47872  grimco  47873  uhgrimedgi  47874  isuspgrim0  47878  upgrimwlklem5  47885  uhgrimisgrgriclem  47914  clnbgrgrimlem  47917  clnbgrgrim  47918  grimedg  47919  uspgrlimlem3  47974  uspgrlimlem4  47975  grlimedgclnbgr  47979  grlimgrtrilem2  47986  grlimgrtri  47987  grilcbri2  47995  grlicsym  47997  grlictr  47999  clnbgr3stgrgrlim  48003  clnbgr3stgrgrlic  48004  lcosslsp  48423  linindslinci  48433  lindslinindsimp1  48442  ldepsnlinclem1  48490  ldepsnlinclem2  48491  iscnrm3r  48932  initc  49076  termc2  49503