Theorem rspcv 3579

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082

This theorem is used by:  rspccv  3580  rspcva  3581  rspccva  3582  rspcdva  3584  rspc2v  3594  rspc3v  3599  rspc4v  3603  rr19.3v  3628  rr19.28v  3629  rspsbc  3833  rspc2vd  3902  intmin  4935  ralxfrALT  5388  somo  5610  fr2nr  5640  weniso  7363  fr3nr  7777  limuni3  7854  tfinds  7862  funcnvuni  7935  resf1extb  7937  poseq  8160  soseq  8161  suppfnss  8191  onnseq  8337  smo11  8357  tfrlem9  8378  tz7.49  8438  omeulem1  8573  oeordi  8579  naddelim  8679  nneneq  9197  frfi  9252  unblem2  9260  unbnn2  9264  ordiso2  9484  cantnflem1  9665  ttrcltr  9692  ttrclss  9696  ttrclselem2  9702  frins3  9734  rankunb  9829  tcrank  9863  scottex  9869  carduni  9983  dfac8alem  10029  alephinit  10095  aceq3lem  10120  dfac5  10128  dfac12r  10146  dfac12k  10147  pwsdompw  10202  cflm  10248  isf32lem1  10352  isf32lem2  10353  isf34lem4  10376  hsmexlem4  10428  axcc3  10437  domtriomlem  10441  axdc3lem2  10450  axdc4lem  10454  axcclem  10456  axdclem  10518  alephval2  10572  winainflem  10693  eltskm  10843  squeeze0  12133  lbreu  12180  nnsub  12295  ublbneg  12973  zmax  12985  zbtwnre  12986  xrub  13354  infmremnf  13386  infmrp1  13387  fzrevral  13657  axdc4uzlem  14037  faclbnd4lem4  14350  ccatalpha  14650  wrdind  14781  wrd2ind  14782  reuccatpfxs1lem  14805  recan  15412  cau3lem  15430  caubnd2  15433  climrlim2  15622  climshftlem  15649  rlimcld2  15653  subcn2  15670  isercoll  15743  climcau  15746  serf0  15756  iseralt  15760  isumrpcl  15920  clim2prod  15965  ntrivcvgfvn0  15976  sqrt2irr  16327  ndvdssub  16489  dfgcd2  16626  lcmf  16713  lcmfunsnlem1  16717  lcmfunsnlem2lem1  16718  lcmfunsnlem2lem2  16719  lcmfdvdsb  16723  coprmgcdb  16729  coprmdvds1  16732  coprmprod  16741  coprmproddvdslem  16742  nprm  16768  dvdsprm  16784  coprm  16792  pcmpt  16974  pcmptdvds  16976  pcfac  16981  prmpwdvds  16986  unbenlem  16990  vdwlem10  17072  vdwlem13  17075  vdwnnlem1  17077  prmdvdsprmop  17125  prmgaplem7  17139  catideu  17753  initoid  18080  termoid  18081  initoeu1  18090  termoeu1  18097  isdrs2  18384  lublecllem  18436  lubun  18593  lidrididd  18754  mgmidpfod  18760  sgrp2rid2ex  19026  dfgrp2  19073  grpidinv2  19108  dfgrp3lem  19148  issubg4  19256  efgi  19833  efgi2  19839  dprdss  20145  srgrz  20333  srglz  20334  srgisid  20335  rrgeq0i  20848  isdomn4  20864  isdrng3lem2  20902  islmodd  21037  rmodislmod  21101  islmhm2  21209  rnglidlmcl  21391  ip2eq  21853  mvrf1  22185  psdmul  22379  cply1mul  22506  isclo2  23295  cnpnei  23471  cncls  23481  lmss  23505  cnt0  23553  isnrm2  23565  isreg2  23584  tgcmp  23608  uncmp  23610  dfconn2  23626  1stcclb  23651  2ndcctbss  23663  comppfsc  23740  kgencn2  23765  ptpjpre1  23779  txlm  23856  kqfvima  23938  kqt0lem  23944  isr0  23945  nrmr0reg  23957  fgss2  24082  isufil2  24116  cfinufil  24136  flimopn  24183  fbflim2  24185  flfneii  24200  cnpflf  24209  fclssscls  24226  fclsnei  24227  fclsrest  24232  flimfnfcls  24236  fclscmp  24238  isfcf  24242  fcfnei  24243  alexsubALTlem3  24257  alexsubALTlem4  24258  alexsubALT  24259  tsmsgsum  24347  tsmsres  24352  tsmsxplem1  24361  ustincl  24416  ustdiag  24417  ustinvel  24418  ustexhalf  24419  cfiluexsm  24497  psmet0  24516  prdsbl  24699  metss  24716  metcnp3  24748  isngp4  24820  nmoi  24936  mulc1cncf  25115  cncfco  25117  lebnumii  25176  iscfil3  25483  iscau2  25487  iscau4  25489  equivcfil  25509  equivcau  25510  lmcau  25523  ismbf  25838  ellimc3  26089  lhop1  26224  dvfsumlem4  26239  dvfsum2  26244  dgrco  26483  fta1  26520  aalioulem2  26547  aalioulem4  26549  ulmclm  26601  ulmshftlem  26603  ulmcaulem  26608  ulmcau  26609  ulmcn  26613  cxploglim  27193  ftalem3  27290  chtub  27427  dchrelbasd  27454  2sqlem6  27638  2sqlem10  27643  dchrisumlema  27703  dchrisumlem2  27705  dchrisumlem3  27706  dchrvmasumlem2  27713  pntpbnd1  27801  pntibnd  27808  pntleml  27826  nolt02o  27910  noresle  27912  nosupbnd1lem1  27923  nosupbnd1lem4  27926  nosupbnd2lem1  27930  nosupbnd2  27931  nocvxminlem  27998  madebdaylemold  28142  n0subs  28607  z12zsodd  28726  brbtwn2  29310  colinearalg  29315  axcontlem4  29372  usgruspgrb  29591  cusgredg  29832  cusgrres  29856  usgredgsscusgredg  29867  fusgrn0degnn0  29907  wlk1walk  30046  wlkres  30076  wlkp1lem6  30084  wlkdlem2  30089  pfxwlk  30093  upgrwlkdvdelem  30149  pthdlem2lem  30180  lfgrn1cycl  30221  wwlksnredwwlkn  30311  wwlksnextproplem2  30326  clwwlkccatlem  30407  clwlkclwwlkf1lem3  30424  clwwisshclwwslemlem  30431  clwwlkf1  30467  clwwlkext2edg  30474  3cyclfrgrrn1  30707  n4cyclfrgr  30713  frgrwopregasn  30738  frgrwopregbsn  30739  isgrpo  30920  blocnilem  31227  ip2eqi  31279  htthlem  31340  hial0  31525  hial02  31526  hial2eq  31529  ocorth  31714  h1de2i  31976  pjjsi  32123  lnopunilem1  32433  lnophmlem1  32439  nmcexi  32449  riesz4i  32486  mdi  32718  mdbr3  32720  mdbr4  32721  dmdi  32725  dmdbr3  32728  dmdbr4  32729  dmdi4  32730  mdslmd1i  32752  atss  32769  atom1d  32776  atmd  32822  sumdmdlem2  32842  cdj1i  32856  cdj3i  32864  fnpreimac  33086  nn0min  33235  archiabllem1a  33575  archiabllem2a  33578  archiabl  33582  isarchiofld  33583  trisecnconstr  34246  crefi  34301  pcmplfin  34314  fmcncfil  34385  sigaclcu  34571  unelsiga  34588  sigapildsys  34617  ldgenpisys  34621  measvun  34664  carsgclctunlem2  34774  sibfima  34793  fnrelpredd  35540  fineqvnttrclse  35594  fineqvinfep  35595  derangenlem  35700  subfacp1lem6  35714  resconn  35775  cvmcov  35792  cvmliftlem3  35816  cvmliftphtlem  35846  satfdmfmla  35929  mclsax  36098  dfon2lem6  36315  fwddifnp1  36694  opnrebl2  36889  nn0prpwlem  36890  nn0prpw  36891  neibastop2lem  36928  neibastop2  36929  filnetlem4  36949  dfttc4  37098  bj-mooreset  37801  bj-ismoored0  37805  dfgcd3  38025  fin2so  38315  poimirlem25  38353  poimirlem29  38357  poimir  38361  mbfresfi  38374  ftc1cnnclem  38399  seqpo  38456  incsequz  38457  mettrifi  38466  geomcau  38468  caushft  38470  sstotbnd2  38483  equivtotbnd  38487  totbndbnd  38498  ismtybndlem  38515  heibor1lem  38518  bfplem2  38532  opidonOLD  38561  exidu1  38565  rngoideu  38612  isdrngo2  38667  unichnidl  38740  lsat0cv  39865  lcvexchlem4  39869  lcvexchlem5  39870  eqlkr3  39933  lub0N  40021  glb0N  40025  cvrnbtwn  40103  ltrneq2  40980  trlval2  40995  lpolsatN  42320  lpolpolsatN  42321  hdmap14lem12  42711  fsuppind  43380  nna4b4nsq  43450  incssnn0  43500  lnmlssfg  43865  unxpwdom3  43880  neik0pk1imk0  44831  ismnushort  45069  fnchoice  45807  monoordxrv  46253  monoord2xrv  46255  limcrecl  46403  fourierdlem54  46932  fourierdlem103  46981  fourierdlem104  46982  euoreqb  47904  smonoord  48172  iccpartlt  48231  iccpartgt  48234  iccpartdisj  48244  paireqne  48318  fmtnodvds  48354  perfectALTVlem2  48545  sbgoldbwt  48600  sbgoldbst  48601  sgoldbeven3prm  48606  mogoldbb  48608  nnsum4primesodd  48619  nnsum4primesoddALTV  48620  bgoldbnnsum3prm  48627  bgoldbtbndlem2  48629  bgoldbtbndlem3  48630  bgoldbtbndlem4  48631  bgoldbtbnd  48632  tgblthelfgott  48638  tgoldbach  48640  grimuhgr  48710  grimcnv  48711  grimco  48712  uhgrimedgi  48713  isuspgrim0  48717  upgrimwlklem5  48724  uhgrimisgrgriclem  48753  clnbgrgrimlem  48756  clnbgrgrim  48757  grimedg  48758  uspgrlimlem3  48813  uspgrlimlem4  48814  grlimedgclnbgr  48818  grlimgrtrilem2  48825  grlimgrtri  48826  grilcbri2  48834  grlicsym  48836  grlictr  48838  clnbgr3stgrgrlim  48842  clnbgr3stgrgrlic  48843  lcosslsp  49275  linindslinci  49285  lindslinindsimp1  49294  ldepsnlinclem1  49342  ldepsnlinclem2  49343  iscnrm3r  49783  initc  49926  termc2  50353