Theorem rspcv 3603

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  ∀wral 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057

This theorem is referenced by:  rspccv  3604  rspcva  3605  rspccva  3606  rspcdva  3608  rspc2v  3618  rspc3v  3623  rspc4v  3626  rr19.3v  3653  rr19.28v  3654  rspsbc  3869  rspc2vd  3940  intmin  4966  ralxfrALT  5409  somo  5621  fr2nr  5650  weniso  7356  fr3nr  7766  limuni3  7848  tfinds  7856  funcnvuni  7931  poseq  8155  soseq  8156  suppfnss  8185  onnseq  8356  smo11  8376  tfrlem9  8397  tz7.49  8457  omeulem1  8594  oeordi  8599  naddelim  8698  nneneq  9223  nneneqOLD  9235  frfi  9302  unblem2  9310  unbnn2  9314  xpfiOLD  9332  ordiso2  9524  cantnflem1  9698  ttrcltr  9725  ttrclss  9729  ttrclselem2  9735  frins3  9764  rankunb  9859  tcrank  9893  carduni  9990  dfac8alem  10038  alephinit  10104  aceq3lem  10129  dfac5  10137  dfac12r  10155  dfac12k  10156  pwsdompw  10213  cflm  10259  isf32lem1  10362  isf32lem2  10363  isf34lem4  10386  hsmexlem4  10438  axcc3  10447  domtriomlem  10451  axdc3lem2  10460  axdc4lem  10464  axcclem  10466  axdclem  10528  alephval2  10581  winainflem  10702  eltskm  10852  squeeze0  12133  lbreu  12180  nnsub  12272  ublbneg  12933  zmax  12945  zbtwnre  12946  xrub  13309  infmremnf  13340  infmrp1  13341  fzrevral  13604  axdc4uzlem  13966  faclbnd4lem4  14273  ccatalpha  14561  wrdind  14690  wrd2ind  14691  reuccatpfxs1lem  14714  recan  15301  cau3lem  15319  caubnd2  15322  climrlim2  15509  climshftlem  15536  rlimcld2  15540  subcn2  15557  isercoll  15632  climcau  15635  serf0  15645  iseralt  15649  isumrpcl  15807  clim2prod  15852  ntrivcvgfvn0  15863  sqrt2irr  16211  ndvdssub  16371  dfgcd2  16507  lcmf  16589  lcmfunsnlem1  16593  lcmfunsnlem2lem1  16594  lcmfunsnlem2lem2  16595  lcmfdvdsb  16599  coprmgcdb  16605  coprmdvds1  16608  coprmprod  16617  coprmproddvdslem  16618  nprm  16644  dvdsprm  16659  coprm  16667  pcmpt  16846  pcmptdvds  16848  pcfac  16853  prmpwdvds  16858  unbenlem  16862  vdwlem10  16944  vdwlem13  16947  vdwnnlem1  16949  prmdvdsprmop  16997  prmgaplem7  17011  catideu  17640  initoid  17975  termoid  17976  initoeu1  17985  termoeu1  17992  isdrs2  18283  lublecllem  18337  lubun  18492  lidrididd  18615  sgrp2rid2ex  18864  dfgrp2  18904  grpidinv2  18939  dfgrp3lem  18978  issubg4  19084  efgi  19658  efgi2  19664  dprdss  19970  srgrz  20131  srglz  20132  srgisid  20133  islmodd  20731  rmodislmod  20795  rmodislmodOLD  20796  islmhm2  20905  rnglidlmcl  21094  rrgeq0i  21218  isdomn4  21231  ip2eq  21565  mvrf1  21906  cply1mul  22189  isclo2  22966  cnpnei  23142  cncls  23152  lmss  23176  cnt0  23224  isnrm2  23236  isreg2  23255  tgcmp  23279  uncmp  23281  dfconn2  23297  1stcclb  23322  2ndcctbss  23333  comppfsc  23410  kgencn2  23435  ptpjpre1  23449  txlm  23526  kqfvima  23608  kqt0lem  23614  isr0  23615  nrmr0reg  23627  fgss2  23752  isufil2  23786  cfinufil  23806  flimopn  23853  fbflim2  23855  flfneii  23870  cnpflf  23879  fclssscls  23896  fclsnei  23897  fclsrest  23902  flimfnfcls  23906  fclscmp  23908  isfcf  23912  fcfnei  23913  alexsubALTlem3  23927  alexsubALTlem4  23928  alexsubALT  23929  tsmsgsum  24017  tsmsres  24022  tsmsxplem1  24031  ustincl  24086  ustdiag  24087  ustinvel  24088  ustexhalf  24089  cfiluexsm  24169  psmet0  24188  prdsbl  24374  metss  24391  metcnp3  24423  isngp4  24495  nmoi  24619  mulc1cncf  24799  cncfco  24801  lebnumii  24866  iscfil3  25175  iscau2  25179  iscau4  25181  equivcfil  25201  equivcau  25202  lmcau  25215  ismbf  25531  ellimc3  25782  lhop1  25921  dvfsumlem4  25938  dvfsum2  25943  dgrco  26184  fta1  26217  aalioulem2  26242  aalioulem4  26244  ulmclm  26297  ulmshftlem  26299  ulmcaulem  26304  ulmcau  26305  ulmcn  26309  cxploglim  26884  ftalem3  26981  chtub  27119  dchrelbasd  27146  2sqlem6  27330  2sqlem10  27335  dchrisumlema  27395  dchrisumlem2  27397  dchrisumlem3  27398  dchrvmasumlem2  27405  pntpbnd1  27493  pntibnd  27500  pntleml  27518  nolt02o  27602  noresle  27604  nosupbnd1lem1  27615  nosupbnd1lem4  27618  nosupbnd2lem1  27622  nosupbnd2  27623  nocvxminlem  27684  madebdaylemold  27798  brbtwn2  28690  colinearalg  28695  axcontlem4  28752  usgruspgrb  28970  cusgredg  29211  cusgrres  29236  usgredgsscusgredg  29247  fusgrn0degnn0  29287  wlk1walk  29427  wlkres  29458  wlkp1lem6  29466  wlkdlem2  29471  upgrwlkdvdelem  29524  pthdlem2lem  29555  lfgrn1cycl  29590  wwlksnredwwlkn  29680  wwlksnextproplem2  29695  clwwlkccatlem  29773  clwlkclwwlkf1lem3  29790  clwwisshclwwslemlem  29797  clwwlkf1  29833  clwwlkext2edg  29840  3cyclfrgrrn1  30069  n4cyclfrgr  30075  frgrwopregasn  30100  frgrwopregbsn  30101  isgrpo  30281  blocnilem  30588  ip2eqi  30640  htthlem  30701  hial0  30886  hial02  30887  hial2eq  30890  ocorth  31075  h1de2i  31337  pjjsi  31484  lnopunilem1  31794  lnophmlem1  31800  nmcexi  31810  riesz4i  31847  mdi  32079  mdbr3  32081  mdbr4  32082  dmdi  32086  dmdbr3  32089  dmdbr4  32090  dmdi4  32091  mdslmd1i  32113  atss  32130  atom1d  32137  atmd  32183  sumdmdlem2  32203  cdj1i  32217  cdj3i  32225  fnpreimac  32427  nn0min  32552  archiabllem1a  32864  archiabllem2a  32867  archiabl  32871  isarchiofld  32959  crefi  33371  pcmplfin  33384  fmcncfil  33455  sigaclcu  33659  unelsiga  33676  sigapildsys  33704  ldgenpisys  33708  measvun  33751  carsgclctunlem2  33862  sibfima  33881  fnrelpredd  34635  pfxwlk  34656  derangenlem  34704  subfacp1lem6  34718  resconn  34779  cvmcov  34796  cvmliftlem3  34820  cvmliftphtlem  34850  satfdmfmla  34933  mclsax  35102  dfon2lem6  35307  fwddifnp1  35684  opnrebl2  35728  nn0prpwlem  35729  nn0prpw  35730  neibastop2lem  35767  neibastop2  35768  filnetlem4  35788  bj-mooreset  36504  bj-ismoored0  36508  dfgcd3  36726  fin2so  37002  poimirlem25  37040  poimirlem29  37044  poimir  37048  mbfresfi  37061  ftc1cnnclem  37086  seqpo  37142  incsequz  37143  mettrifi  37152  geomcau  37154  caushft  37156  sstotbnd2  37169  equivtotbnd  37173  totbndbnd  37184  ismtybndlem  37201  heibor1lem  37204  bfplem2  37218  opidonOLD  37247  exidu1  37251  rngoideu  37298  isdrngo2  37353  unichnidl  37426  lsat0cv  38429  lcvexchlem4  38433  lcvexchlem5  38434  eqlkr3  38497  lub0N  38585  glb0N  38589  cvrnbtwn  38667  ltrneq2  39545  trlval2  39560  lpolsatN  40885  lpolpolsatN  40886  hdmap14lem12  41276  fsuppind  41735  nna4b4nsq  41996  incssnn0  42043  lnmlssfg  42416  unxpwdom3  42431  neik0pk1imk0  43390  ismnushort  43651  fnchoice  44304  monoordxrv  44777  monoord2xrv  44779  limcrecl  44930  fourierdlem54  45461  fourierdlem103  45510  fourierdlem104  45511  euoreqb  46402  smonoord  46624  iccpartlt  46677  iccpartgt  46680  iccpartdisj  46690  paireqne  46764  fmtnodvds  46797  perfectALTVlem2  46975  sbgoldbwt  47030  sbgoldbst  47031  sgoldbeven3prm  47036  mogoldbb  47038  nnsum4primesodd  47049  nnsum4primesoddALTV  47050  bgoldbnnsum3prm  47057  bgoldbtbndlem2  47059  bgoldbtbndlem3  47060  bgoldbtbndlem4  47061  bgoldbtbnd  47062  tgblthelfgott  47068  tgoldbach  47070  isuspgrim0  47083  grimuhgr  47089  grimcnv  47090  grimco  47091  lcosslsp  47419  linindslinci  47429  lindslinindsimp1  47438  ldepsnlinclem1  47486  ldepsnlinclem2  47487  iscnrm3r  47880