Theorem rspcv 3577

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2176, ax-11 2192, ax-12 2213. (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 23	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵)
2		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	adantl 486	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcdv 3573	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080

This theorem is referenced by:  rspccv  3578  rspcva  3579  rspccva  3580  rspcdva  3582  rspc2v  3592  rspc3v  3597  rspc4v  3601  rr19.3v  3626  rr19.28v  3627  rspsbc  3832  rspc2vd  3901  intmin  4933  ralxfrALT  5386  somo  5608  fr2nr  5638  weniso  7352  fr3nr  7767  limuni3  7844  tfinds  7852  funcnvuni  7925  resf1extb  7927  poseq  8150  soseq  8151  suppfnss  8181  onnseq  8327  smo11  8347  tfrlem9  8368  tz7.49  8428  omeulem1  8563  oeordi  8569  naddelim  8669  nneneq  9186  frfi  9241  unblem2  9249  unbnn2  9253  ordiso2  9473  cantnflem1  9654  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  frins3  9723  rankunb  9818  tcrank  9852  carduni  9963  dfac8alem  10009  alephinit  10075  aceq3lem  10100  dfac5  10108  dfac12r  10126  dfac12k  10127  pwsdompw  10182  cflm  10228  isf32lem1  10332  isf32lem2  10333  isf34lem4  10356  hsmexlem4  10408  axcc3  10417  domtriomlem  10421  axdc3lem2  10430  axdc4lem  10434  axcclem  10436  axdclem  10498  alephval2  10552  winainflem  10673  eltskm  10823  squeeze0  12113  lbreu  12160  nnsub  12275  ublbneg  12952  zmax  12964  zbtwnre  12965  xrub  13333  infmremnf  13365  infmrp1  13366  fzrevral  13636  axdc4uzlem  14015  faclbnd4lem4  14328  ccatalpha  14627  wrdind  14755  wrd2ind  14756  reuccatpfxs1lem  14779  recan  15384  cau3lem  15402  caubnd2  15405  climrlim2  15594  climshftlem  15621  rlimcld2  15625  subcn2  15642  isercoll  15715  climcau  15718  serf0  15728  iseralt  15732  isumrpcl  15893  clim2prod  15938  ntrivcvgfvn0  15949  sqrt2irr  16300  ndvdssub  16462  dfgcd2  16599  lcmf  16686  lcmfunsnlem1  16690  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  lcmfdvdsb  16696  coprmgcdb  16702  coprmdvds1  16705  coprmprod  16714  coprmproddvdslem  16715  nprm  16741  dvdsprm  16757  coprm  16765  pcmpt  16947  pcmptdvds  16949  pcfac  16954  prmpwdvds  16959  unbenlem  16963  vdwlem10  17045  vdwlem13  17048  vdwnnlem1  17050  prmdvdsprmop  17098  prmgaplem7  17112  catideu  17726  initoid  18053  termoid  18054  initoeu1  18063  termoeu1  18070  isdrs2  18357  lublecllem  18409  lubun  18566  lidrididd  18723  sgrp2rid2ex  18984  dfgrp2  19024  grpidinv2  19059  dfgrp3lem  19099  issubg4  19207  efgi  19784  efgi2  19790  dprdss  20096  srgrz  20284  srglz  20285  srgisid  20286  rrgeq0i  20798  isdomn4  20814  isdrng3lem2  20852  islmodd  20987  rmodislmod  21051  islmhm2  21159  rnglidlmcl  21341  ip2eq  21803  mvrf1  22135  psdmul  22329  cply1mul  22456  isclo2  23245  cnpnei  23421  cncls  23431  lmss  23455  cnt0  23503  isnrm2  23515  isreg2  23534  tgcmp  23558  uncmp  23560  dfconn2  23576  1stcclb  23601  2ndcctbss  23612  comppfsc  23689  kgencn2  23714  ptpjpre1  23728  txlm  23805  kqfvima  23887  kqt0lem  23893  isr0  23894  nrmr0reg  23906  fgss2  24031  isufil2  24065  cfinufil  24085  flimopn  24132  fbflim2  24134  flfneii  24149  cnpflf  24158  fclssscls  24175  fclsnei  24176  fclsrest  24181  flimfnfcls  24185  fclscmp  24187  isfcf  24191  fcfnei  24192  alexsubALTlem3  24206  alexsubALTlem4  24207  alexsubALT  24208  tsmsgsum  24296  tsmsres  24301  tsmsxplem1  24310  ustincl  24365  ustdiag  24366  ustinvel  24367  ustexhalf  24368  cfiluexsm  24446  psmet0  24465  prdsbl  24648  metss  24665  metcnp3  24697  isngp4  24769  nmoi  24885  mulc1cncf  25064  cncfco  25066  lebnumii  25125  iscfil3  25432  iscau2  25436  iscau4  25438  equivcfil  25458  equivcau  25459  lmcau  25472  ismbf  25787  ellimc3  26038  lhop1  26173  dvfsumlem4  26188  dvfsum2  26193  dgrco  26432  fta1  26469  aalioulem2  26496  aalioulem4  26498  ulmclm  26550  ulmshftlem  26552  ulmcaulem  26557  ulmcau  26558  ulmcn  26562  cxploglim  27142  ftalem3  27239  chtub  27376  dchrelbasd  27403  2sqlem6  27587  2sqlem10  27592  dchrisumlema  27652  dchrisumlem2  27654  dchrisumlem3  27655  dchrvmasumlem2  27662  pntpbnd1  27750  pntibnd  27757  pntleml  27775  nolt02o  27859  noresle  27861  nosupbnd1lem1  27872  nosupbnd1lem4  27875  nosupbnd2lem1  27879  nosupbnd2  27880  nocvxminlem  27947  madebdaylemold  28091  n0subs  28556  z12zsodd  28675  brbtwn2  29255  colinearalg  29260  axcontlem4  29317  usgruspgrb  29533  cusgredg  29774  cusgrres  29798  usgredgsscusgredg  29809  fusgrn0degnn0  29849  wlk1walk  29988  wlkres  30018  wlkp1lem6  30026  wlkdlem2  30031  upgrwlkdvdelem  30085  pthdlem2lem  30116  lfgrn1cycl  30154  wwlksnredwwlkn  30244  wwlksnextproplem2  30259  clwwlkccatlem  30340  clwlkclwwlkf1lem3  30357  clwwisshclwwslemlem  30364  clwwlkf1  30400  clwwlkext2edg  30407  3cyclfrgrrn1  30636  n4cyclfrgr  30642  frgrwopregasn  30667  frgrwopregbsn  30668  isgrpo  30849  blocnilem  31156  ip2eqi  31208  htthlem  31269  hial0  31454  hial02  31455  hial2eq  31458  ocorth  31643  h1de2i  31905  pjjsi  32052  lnopunilem1  32362  lnophmlem1  32368  nmcexi  32378  riesz4i  32415  mdi  32647  mdbr3  32649  mdbr4  32650  dmdi  32654  dmdbr3  32657  dmdbr4  32658  dmdi4  32659  mdslmd1i  32681  atss  32698  atom1d  32705  atmd  32751  sumdmdlem2  32771  cdj1i  32785  cdj3i  32793  fnpreimac  33015  nn0min  33165  archiabllem1a  33511  archiabllem2a  33514  archiabl  33518  isarchiofld  33519  trisecnconstr  34182  crefi  34237  pcmplfin  34250  fmcncfil  34321  sigaclcu  34507  unelsiga  34524  sigapildsys  34552  ldgenpisys  34556  measvun  34599  carsgclctunlem2  34709  sibfima  34728  fnrelpredd  35482  fineqvnttrclse  35537  fineqvinfep  35538  pfxwlk  35616  derangenlem  35663  subfacp1lem6  35677  resconn  35738  cvmcov  35755  cvmliftlem3  35779  cvmliftphtlem  35809  satfdmfmla  35892  mclsax  36061  dfon2lem6  36278  fwddifnp1  36657  opnrebl2  36832  nn0prpwlem  36833  nn0prpw  36834  neibastop2lem  36871  neibastop2  36872  filnetlem4  36892  dfttc4  37041  bj-mooreset  37744  bj-ismoored0  37748  dfgcd3  37968  fin2so  38258  poimirlem25  38296  poimirlem29  38300  poimir  38304  mbfresfi  38317  ftc1cnnclem  38342  seqpo  38398  incsequz  38399  mettrifi  38408  geomcau  38410  caushft  38412  sstotbnd2  38425  equivtotbnd  38429  totbndbnd  38440  ismtybndlem  38457  heibor1lem  38460  bfplem2  38474  opidonOLD  38503  exidu1  38507  rngoideu  38554  isdrngo2  38609  unichnidl  38682  lsat0cv  39807  lcvexchlem4  39811  lcvexchlem5  39812  eqlkr3  39875  lub0N  39963  glb0N  39967  cvrnbtwn  40045  ltrneq2  40922  trlval2  40937  lpolsatN  42262  lpolpolsatN  42263  hdmap14lem12  42653  fsuppind  43322  nna4b4nsq  43392  incssnn0  43442  lnmlssfg  43807  unxpwdom3  43822  neik0pk1imk0  44773  ismnushort  45011  fnchoice  45749  monoordxrv  46195  monoord2xrv  46197  limcrecl  46345  fourierdlem54  46874  fourierdlem103  46923  fourierdlem104  46924  euoreqb  47846  smonoord  48114  iccpartlt  48173  iccpartgt  48176  iccpartdisj  48186  paireqne  48260  fmtnodvds  48296  perfectALTVlem2  48487  sbgoldbwt  48542  sbgoldbst  48543  sgoldbeven3prm  48548  mogoldbb  48550  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  bgoldbnnsum3prm  48569  bgoldbtbndlem2  48571  bgoldbtbndlem3  48572  bgoldbtbndlem4  48573  bgoldbtbnd  48574  tgblthelfgott  48580  tgoldbach  48582  grimuhgr  48652  grimcnv  48653  grimco  48654  uhgrimedgi  48655  isuspgrim0  48659  upgrimwlklem5  48666  uhgrimisgrgriclem  48695  clnbgrgrimlem  48698  clnbgrgrim  48699  grimedg  48700  uspgrlimlem3  48755  uspgrlimlem4  48756  grlimedgclnbgr  48760  grlimgrtrilem2  48767  grlimgrtri  48768  grilcbri2  48776  grlicsym  48778  grlictr  48780  clnbgr3stgrgrlim  48784  clnbgr3stgrgrlic  48785  lcosslsp  49218  linindslinci  49228  lindslinindsimp1  49237  ldepsnlinclem1  49285  ldepsnlinclem2  49286  iscnrm3r  49726  initc  49869  termc2  50296