Theorem rspcv 3572

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  rspccv  3573  rspcva  3574  rspccva  3575  rspcdva  3577  rspc2v  3587  rspc3v  3592  rspc4v  3596  rr19.3v  3621  rr19.28v  3622  rspsbc  3829  rspc2vd  3897  intmin  4923  ralxfrALT  5360  somo  5571  fr2nr  5601  weniso  7300  fr3nr  7717  limuni3  7794  tfinds  7802  funcnvuni  7874  resf1extb  7876  poseq  8100  soseq  8101  suppfnss  8131  onnseq  8276  smo11  8296  tfrlem9  8316  tz7.49  8376  omeulem1  8509  oeordi  8515  naddelim  8614  nneneq  9130  frfi  9185  unblem2  9193  unbnn2  9197  ordiso2  9420  cantnflem1  9598  ttrcltr  9625  ttrclss  9629  ttrclselem2  9635  frins3  9667  rankunb  9762  tcrank  9796  carduni  9893  dfac8alem  9939  alephinit  10005  aceq3lem  10030  dfac5  10039  dfac12r  10057  dfac12k  10058  pwsdompw  10113  cflm  10160  isf32lem1  10263  isf32lem2  10264  isf34lem4  10287  hsmexlem4  10339  axcc3  10348  domtriomlem  10352  axdc3lem2  10361  axdc4lem  10365  axcclem  10367  axdclem  10429  alephval2  10483  winainflem  10604  eltskm  10754  squeeze0  12045  lbreu  12092  nnsub  12189  ublbneg  12846  zmax  12858  zbtwnre  12859  xrub  13227  infmremnf  13259  infmrp1  13260  fzrevral  13528  axdc4uzlem  13906  faclbnd4lem4  14219  ccatalpha  14517  wrdind  14645  wrd2ind  14646  reuccatpfxs1lem  14669  recan  15260  cau3lem  15278  caubnd2  15281  climrlim2  15470  climshftlem  15497  rlimcld2  15501  subcn2  15518  isercoll  15591  climcau  15594  serf0  15604  iseralt  15608  isumrpcl  15766  clim2prod  15811  ntrivcvgfvn0  15822  sqrt2irr  16174  ndvdssub  16336  dfgcd2  16473  lcmf  16560  lcmfunsnlem1  16564  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  lcmfdvdsb  16570  coprmgcdb  16576  coprmdvds1  16579  coprmprod  16588  coprmproddvdslem  16589  nprm  16615  dvdsprm  16630  coprm  16638  pcmpt  16820  pcmptdvds  16822  pcfac  16827  prmpwdvds  16832  unbenlem  16836  vdwlem10  16918  vdwlem13  16921  vdwnnlem1  16923  prmdvdsprmop  16971  prmgaplem7  16985  catideu  17598  initoid  17925  termoid  17926  initoeu1  17935  termoeu1  17942  isdrs2  18229  lublecllem  18281  lubun  18438  lidrididd  18595  sgrp2rid2ex  18852  dfgrp2  18892  grpidinv2  18927  dfgrp3lem  18968  issubg4  19075  efgi  19648  efgi2  19654  dprdss  19960  srgrz  20142  srglz  20143  srgisid  20144  rrgeq0i  20632  isdomn4  20649  islmodd  20817  rmodislmod  20881  islmhm2  20990  rnglidlmcl  21171  ip2eq  21608  mvrf1  21941  psdmul  22109  cply1mul  22240  isclo2  23032  cnpnei  23208  cncls  23218  lmss  23242  cnt0  23290  isnrm2  23302  isreg2  23321  tgcmp  23345  uncmp  23347  dfconn2  23363  1stcclb  23388  2ndcctbss  23399  comppfsc  23476  kgencn2  23501  ptpjpre1  23515  txlm  23592  kqfvima  23674  kqt0lem  23680  isr0  23681  nrmr0reg  23693  fgss2  23818  isufil2  23852  cfinufil  23872  flimopn  23919  fbflim2  23921  flfneii  23936  cnpflf  23945  fclssscls  23962  fclsnei  23963  fclsrest  23968  flimfnfcls  23972  fclscmp  23974  isfcf  23978  fcfnei  23979  alexsubALTlem3  23993  alexsubALTlem4  23994  alexsubALT  23995  tsmsgsum  24083  tsmsres  24088  tsmsxplem1  24097  ustincl  24152  ustdiag  24153  ustinvel  24154  ustexhalf  24155  cfiluexsm  24233  psmet0  24252  prdsbl  24435  metss  24452  metcnp3  24484  isngp4  24556  nmoi  24672  mulc1cncf  24854  cncfco  24856  lebnumii  24921  iscfil3  25229  iscau2  25233  iscau4  25235  equivcfil  25255  equivcau  25256  lmcau  25269  ismbf  25585  ellimc3  25836  lhop1  25975  dvfsumlem4  25992  dvfsum2  25997  dgrco  26237  fta1  26272  aalioulem2  26297  aalioulem4  26299  ulmclm  26352  ulmshftlem  26354  ulmcaulem  26359  ulmcau  26360  ulmcn  26364  cxploglim  26944  ftalem3  27041  chtub  27179  dchrelbasd  27206  2sqlem6  27390  2sqlem10  27395  dchrisumlema  27455  dchrisumlem2  27457  dchrisumlem3  27458  dchrvmasumlem2  27465  pntpbnd1  27553  pntibnd  27560  pntleml  27578  nolt02o  27663  noresle  27665  nosupbnd1lem1  27676  nosupbnd1lem4  27679  nosupbnd2lem1  27683  nosupbnd2  27684  nocvxminlem  27750  madebdaylemold  27894  n0subs  28359  z12zsodd  28478  brbtwn2  28978  colinearalg  28983  axcontlem4  29040  usgruspgrb  29256  cusgredg  29497  cusgrres  29522  usgredgsscusgredg  29533  fusgrn0degnn0  29573  wlk1walk  29712  wlkres  29742  wlkp1lem6  29750  wlkdlem2  29755  upgrwlkdvdelem  29809  pthdlem2lem  29840  lfgrn1cycl  29878  wwlksnredwwlkn  29968  wwlksnextproplem2  29983  clwwlkccatlem  30064  clwlkclwwlkf1lem3  30081  clwwisshclwwslemlem  30088  clwwlkf1  30124  clwwlkext2edg  30131  3cyclfrgrrn1  30360  n4cyclfrgr  30366  frgrwopregasn  30391  frgrwopregbsn  30392  isgrpo  30572  blocnilem  30879  ip2eqi  30931  htthlem  30992  hial0  31177  hial02  31178  hial2eq  31181  ocorth  31366  h1de2i  31628  pjjsi  31775  lnopunilem1  32085  lnophmlem1  32091  nmcexi  32101  riesz4i  32138  mdi  32370  mdbr3  32372  mdbr4  32373  dmdi  32377  dmdbr3  32380  dmdbr4  32381  dmdi4  32382  mdslmd1i  32404  atss  32421  atom1d  32428  atmd  32474  sumdmdlem2  32494  cdj1i  32508  cdj3i  32516  fnpreimac  32749  nn0min  32901  archiabllem1a  33273  archiabllem2a  33276  archiabl  33280  isarchiofld  33281  trisecnconstr  33949  crefi  34004  pcmplfin  34017  fmcncfil  34088  sigaclcu  34274  unelsiga  34291  sigapildsys  34319  ldgenpisys  34323  measvun  34366  carsgclctunlem2  34476  sibfima  34495  fnrelpredd  35247  fineqvnttrclse  35280  fineqvinfep  35281  pfxwlk  35318  derangenlem  35365  subfacp1lem6  35379  resconn  35440  cvmcov  35457  cvmliftlem3  35481  cvmliftphtlem  35511  satfdmfmla  35594  mclsax  35763  dfon2lem6  35980  fwddifnp1  36359  opnrebl2  36515  nn0prpwlem  36516  nn0prpw  36517  neibastop2lem  36554  neibastop2  36555  filnetlem4  36575  bj-mooreset  37307  bj-ismoored0  37311  dfgcd3  37529  fin2so  37808  poimirlem25  37846  poimirlem29  37850  poimir  37854  mbfresfi  37867  ftc1cnnclem  37892  seqpo  37948  incsequz  37949  mettrifi  37958  geomcau  37960  caushft  37962  sstotbnd2  37975  equivtotbnd  37979  totbndbnd  37990  ismtybndlem  38007  heibor1lem  38010  bfplem2  38024  opidonOLD  38053  exidu1  38057  rngoideu  38104  isdrngo2  38159  unichnidl  38232  lsat0cv  39293  lcvexchlem4  39297  lcvexchlem5  39298  eqlkr3  39361  lub0N  39449  glb0N  39453  cvrnbtwn  39531  ltrneq2  40408  trlval2  40423  lpolsatN  41748  lpolpolsatN  41749  hdmap14lem12  42139  fsuppind  42833  nna4b4nsq  42903  incssnn0  42953  lnmlssfg  43322  unxpwdom3  43337  neik0pk1imk0  44288  ismnushort  44542  fnchoice  45274  monoordxrv  45725  monoord2xrv  45727  limcrecl  45875  fourierdlem54  46404  fourierdlem103  46453  fourierdlem104  46454  euoreqb  47355  smonoord  47617  iccpartlt  47670  iccpartgt  47673  iccpartdisj  47683  paireqne  47757  fmtnodvds  47790  perfectALTVlem2  47968  sbgoldbwt  48023  sbgoldbst  48024  sgoldbeven3prm  48029  mogoldbb  48031  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  bgoldbnnsum3prm  48050  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  bgoldbtbndlem4  48054  bgoldbtbnd  48055  tgblthelfgott  48061  tgoldbach  48063  grimuhgr  48133  grimcnv  48134  grimco  48135  uhgrimedgi  48136  isuspgrim0  48140  upgrimwlklem5  48147  uhgrimisgrgriclem  48176  clnbgrgrimlem  48179  clnbgrgrim  48180  grimedg  48181  uspgrlimlem3  48236  uspgrlimlem4  48237  grlimedgclnbgr  48241  grlimgrtrilem2  48248  grlimgrtri  48249  grilcbri2  48257  grlicsym  48259  grlictr  48261  clnbgr3stgrgrlim  48265  clnbgr3stgrgrlic  48266  lcosslsp  48684  linindslinci  48694  lindslinindsimp1  48703  ldepsnlinclem1  48751  ldepsnlinclem2  48752  iscnrm3r  49193  initc  49336  termc2  49763