Theorem rspcv 3617

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059

This theorem is referenced by:  rspccv  3618  rspcva  3619  rspccva  3620  rspcdva  3622  rspc2v  3632  rspc3v  3637  rspc4v  3641  rr19.3v  3666  rr19.28v  3667  rspsbc  3887  rspc2vd  3958  intmin  4972  ralxfrALT  5420  somo  5634  fr2nr  5665  weniso  7373  fr3nr  7790  limuni3  7872  tfinds  7880  funcnvuni  7954  poseq  8181  soseq  8182  suppfnss  8212  onnseq  8382  smo11  8402  tfrlem9  8423  tz7.49  8483  omeulem1  8618  oeordi  8623  naddelim  8722  nneneq  9243  nneneqOLD  9255  frfi  9318  unblem2  9326  unbnn2  9330  xpfiOLD  9356  ordiso2  9552  cantnflem1  9726  ttrcltr  9753  ttrclss  9757  ttrclselem2  9763  frins3  9792  rankunb  9887  tcrank  9921  carduni  10018  dfac8alem  10066  alephinit  10132  aceq3lem  10157  dfac5  10166  dfac12r  10184  dfac12k  10185  pwsdompw  10240  cflm  10287  isf32lem1  10390  isf32lem2  10391  isf34lem4  10414  hsmexlem4  10466  axcc3  10475  domtriomlem  10479  axdc3lem2  10488  axdc4lem  10492  axcclem  10494  axdclem  10556  alephval2  10609  winainflem  10730  eltskm  10880  squeeze0  12168  lbreu  12215  nnsub  12307  ublbneg  12972  zmax  12984  zbtwnre  12985  xrub  13350  infmremnf  13381  infmrp1  13382  fzrevral  13648  axdc4uzlem  14020  faclbnd4lem4  14331  ccatalpha  14627  wrdind  14756  wrd2ind  14757  reuccatpfxs1lem  14780  recan  15371  cau3lem  15389  caubnd2  15392  climrlim2  15579  climshftlem  15606  rlimcld2  15610  subcn2  15627  isercoll  15700  climcau  15703  serf0  15713  iseralt  15717  isumrpcl  15875  clim2prod  15920  ntrivcvgfvn0  15931  sqrt2irr  16281  ndvdssub  16442  dfgcd2  16579  lcmf  16666  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfdvdsb  16676  coprmgcdb  16682  coprmdvds1  16685  coprmprod  16694  coprmproddvdslem  16695  nprm  16721  dvdsprm  16736  coprm  16744  pcmpt  16925  pcmptdvds  16927  pcfac  16932  prmpwdvds  16937  unbenlem  16941  vdwlem10  17023  vdwlem13  17026  vdwnnlem1  17028  prmdvdsprmop  17076  prmgaplem7  17090  catideu  17719  initoid  18054  termoid  18055  initoeu1  18064  termoeu1  18071  isdrs2  18363  lublecllem  18417  lubun  18572  lidrididd  18695  sgrp2rid2ex  18952  dfgrp2  18992  grpidinv2  19027  dfgrp3lem  19068  issubg4  19175  efgi  19751  efgi2  19757  dprdss  20063  srgrz  20224  srglz  20225  srgisid  20226  rrgeq0i  20715  isdomn4  20732  islmodd  20880  rmodislmod  20944  rmodislmodOLD  20945  islmhm2  21054  rnglidlmcl  21243  ip2eq  21688  mvrf1  22023  psdmul  22187  cply1mul  22315  isclo2  23111  cnpnei  23287  cncls  23297  lmss  23321  cnt0  23369  isnrm2  23381  isreg2  23400  tgcmp  23424  uncmp  23426  dfconn2  23442  1stcclb  23467  2ndcctbss  23478  comppfsc  23555  kgencn2  23580  ptpjpre1  23594  txlm  23671  kqfvima  23753  kqt0lem  23759  isr0  23760  nrmr0reg  23772  fgss2  23897  isufil2  23931  cfinufil  23951  flimopn  23998  fbflim2  24000  flfneii  24015  cnpflf  24024  fclssscls  24041  fclsnei  24042  fclsrest  24047  flimfnfcls  24051  fclscmp  24053  isfcf  24057  fcfnei  24058  alexsubALTlem3  24072  alexsubALTlem4  24073  alexsubALT  24074  tsmsgsum  24162  tsmsres  24167  tsmsxplem1  24176  ustincl  24231  ustdiag  24232  ustinvel  24233  ustexhalf  24234  cfiluexsm  24314  psmet0  24333  prdsbl  24519  metss  24536  metcnp3  24568  isngp4  24640  nmoi  24764  mulc1cncf  24944  cncfco  24946  lebnumii  25011  iscfil3  25320  iscau2  25324  iscau4  25326  equivcfil  25346  equivcau  25347  lmcau  25360  ismbf  25676  ellimc3  25928  lhop1  26067  dvfsumlem4  26084  dvfsum2  26089  dgrco  26329  fta1  26364  aalioulem2  26389  aalioulem4  26391  ulmclm  26444  ulmshftlem  26446  ulmcaulem  26451  ulmcau  26452  ulmcn  26456  cxploglim  27035  ftalem3  27132  chtub  27270  dchrelbasd  27297  2sqlem6  27481  2sqlem10  27486  dchrisumlema  27546  dchrisumlem2  27548  dchrisumlem3  27549  dchrvmasumlem2  27556  pntpbnd1  27644  pntibnd  27651  pntleml  27669  nolt02o  27754  noresle  27756  nosupbnd1lem1  27767  nosupbnd1lem4  27770  nosupbnd2lem1  27774  nosupbnd2  27775  nocvxminlem  27836  madebdaylemold  27950  n0subs  28374  brbtwn2  28934  colinearalg  28939  axcontlem4  28996  usgruspgrb  29214  cusgredg  29455  cusgrres  29480  usgredgsscusgredg  29491  fusgrn0degnn0  29531  wlk1walk  29671  wlkres  29702  wlkp1lem6  29710  wlkdlem2  29715  upgrwlkdvdelem  29768  pthdlem2lem  29799  lfgrn1cycl  29834  wwlksnredwwlkn  29924  wwlksnextproplem2  29939  clwwlkccatlem  30017  clwlkclwwlkf1lem3  30034  clwwisshclwwslemlem  30041  clwwlkf1  30077  clwwlkext2edg  30084  3cyclfrgrrn1  30313  n4cyclfrgr  30319  frgrwopregasn  30344  frgrwopregbsn  30345  isgrpo  30525  blocnilem  30832  ip2eqi  30884  htthlem  30945  hial0  31130  hial02  31131  hial2eq  31134  ocorth  31319  h1de2i  31581  pjjsi  31728  lnopunilem1  32038  lnophmlem1  32044  nmcexi  32054  riesz4i  32091  mdi  32323  mdbr3  32325  mdbr4  32326  dmdi  32330  dmdbr3  32333  dmdbr4  32334  dmdi4  32335  mdslmd1i  32357  atss  32374  atom1d  32381  atmd  32427  sumdmdlem2  32447  cdj1i  32461  cdj3i  32469  fnpreimac  32687  nn0min  32826  archiabllem1a  33180  archiabllem2a  33183  archiabl  33187  isarchiofld  33326  crefi  33807  pcmplfin  33820  fmcncfil  33891  sigaclcu  34097  unelsiga  34114  sigapildsys  34142  ldgenpisys  34146  measvun  34189  carsgclctunlem2  34300  sibfima  34319  fnrelpredd  35081  pfxwlk  35107  derangenlem  35155  subfacp1lem6  35169  resconn  35230  cvmcov  35247  cvmliftlem3  35271  cvmliftphtlem  35301  satfdmfmla  35384  mclsax  35553  dfon2lem6  35769  fwddifnp1  36146  opnrebl2  36303  nn0prpwlem  36304  nn0prpw  36305  neibastop2lem  36342  neibastop2  36343  filnetlem4  36363  bj-mooreset  37084  bj-ismoored0  37088  dfgcd3  37306  fin2so  37593  poimirlem25  37631  poimirlem29  37635  poimir  37639  mbfresfi  37652  ftc1cnnclem  37677  seqpo  37733  incsequz  37734  mettrifi  37743  geomcau  37745  caushft  37747  sstotbnd2  37760  equivtotbnd  37764  totbndbnd  37775  ismtybndlem  37792  heibor1lem  37795  bfplem2  37809  opidonOLD  37838  exidu1  37842  rngoideu  37889  isdrngo2  37944  unichnidl  38017  lsat0cv  39014  lcvexchlem4  39018  lcvexchlem5  39019  eqlkr3  39082  lub0N  39170  glb0N  39174  cvrnbtwn  39252  ltrneq2  40130  trlval2  40145  lpolsatN  41470  lpolpolsatN  41471  hdmap14lem12  41861  fsuppind  42576  nna4b4nsq  42646  incssnn0  42698  lnmlssfg  43068  unxpwdom3  43083  neik0pk1imk0  44036  ismnushort  44296  fnchoice  44966  monoordxrv  45431  monoord2xrv  45433  limcrecl  45584  fourierdlem54  46115  fourierdlem103  46164  fourierdlem104  46165  euoreqb  47058  smonoord  47295  iccpartlt  47348  iccpartgt  47351  iccpartdisj  47361  paireqne  47435  fmtnodvds  47468  perfectALTVlem2  47646  sbgoldbwt  47701  sbgoldbst  47702  sgoldbeven3prm  47707  mogoldbb  47709  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  bgoldbnnsum3prm  47728  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  bgoldbtbnd  47733  tgblthelfgott  47739  tgoldbach  47741  isuspgrim0  47809  grimuhgr  47815  grimcnv  47816  grimco  47817  uhgrimisgrgriclem  47835  clnbgrgrimlem  47838  clnbgrgrim  47839  grimedg  47840  uspgrlimlem3  47892  uspgrlimlem4  47893  grlimgrtrilem2  47897  grlimgrtri  47898  grilcbri2  47906  grlicsym  47908  grlictr  47910  clnbgr3stgrgrlic  47914  lcosslsp  48283  linindslinci  48293  lindslinindsimp1  48302  ldepsnlinclem1  48350  ldepsnlinclem2  48351  iscnrm3r  48744