Theorem rspcv 3597

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052

This theorem is referenced by:  rspccv  3598  rspcva  3599  rspccva  3600  rspcdva  3602  rspc2v  3612  rspc3v  3617  rspc4v  3621  rr19.3v  3646  rr19.28v  3647  rspsbc  3854  rspc2vd  3922  intmin  4944  ralxfrALT  5385  somo  5600  fr2nr  5631  weniso  7346  fr3nr  7764  limuni3  7845  tfinds  7853  funcnvuni  7926  resf1extb  7928  poseq  8155  soseq  8156  suppfnss  8186  onnseq  8356  smo11  8376  tfrlem9  8397  tz7.49  8457  omeulem1  8592  oeordi  8597  naddelim  8696  nneneq  9218  frfi  9291  unblem2  9299  unbnn2  9303  xpfiOLD  9329  ordiso2  9527  cantnflem1  9701  ttrcltr  9728  ttrclss  9732  ttrclselem2  9738  frins3  9767  rankunb  9862  tcrank  9896  carduni  9993  dfac8alem  10041  alephinit  10107  aceq3lem  10132  dfac5  10141  dfac12r  10159  dfac12k  10160  pwsdompw  10215  cflm  10262  isf32lem1  10365  isf32lem2  10366  isf34lem4  10389  hsmexlem4  10441  axcc3  10450  domtriomlem  10454  axdc3lem2  10463  axdc4lem  10467  axcclem  10469  axdclem  10531  alephval2  10584  winainflem  10705  eltskm  10855  squeeze0  12143  lbreu  12190  nnsub  12282  ublbneg  12947  zmax  12959  zbtwnre  12960  xrub  13326  infmremnf  13358  infmrp1  13359  fzrevral  13627  axdc4uzlem  13999  faclbnd4lem4  14312  ccatalpha  14609  wrdind  14738  wrd2ind  14739  reuccatpfxs1lem  14762  recan  15353  cau3lem  15371  caubnd2  15374  climrlim2  15561  climshftlem  15588  rlimcld2  15592  subcn2  15609  isercoll  15682  climcau  15685  serf0  15695  iseralt  15699  isumrpcl  15857  clim2prod  15902  ntrivcvgfvn0  15913  sqrt2irr  16265  ndvdssub  16426  dfgcd2  16563  lcmf  16650  lcmfunsnlem1  16654  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  lcmfdvdsb  16660  coprmgcdb  16666  coprmdvds1  16669  coprmprod  16678  coprmproddvdslem  16679  nprm  16705  dvdsprm  16720  coprm  16728  pcmpt  16910  pcmptdvds  16912  pcfac  16917  prmpwdvds  16922  unbenlem  16926  vdwlem10  17008  vdwlem13  17011  vdwnnlem1  17013  prmdvdsprmop  17061  prmgaplem7  17075  catideu  17685  initoid  18012  termoid  18013  initoeu1  18022  termoeu1  18029  isdrs2  18316  lublecllem  18368  lubun  18523  lidrididd  18646  sgrp2rid2ex  18903  dfgrp2  18943  grpidinv2  18978  dfgrp3lem  19019  issubg4  19126  efgi  19698  efgi2  19704  dprdss  20010  srgrz  20165  srglz  20166  srgisid  20167  rrgeq0i  20657  isdomn4  20674  islmodd  20821  rmodislmod  20885  islmhm2  20994  rnglidlmcl  21175  ip2eq  21611  mvrf1  21944  psdmul  22102  cply1mul  22232  isclo2  23024  cnpnei  23200  cncls  23210  lmss  23234  cnt0  23282  isnrm2  23294  isreg2  23313  tgcmp  23337  uncmp  23339  dfconn2  23355  1stcclb  23380  2ndcctbss  23391  comppfsc  23468  kgencn2  23493  ptpjpre1  23507  txlm  23584  kqfvima  23666  kqt0lem  23672  isr0  23673  nrmr0reg  23685  fgss2  23810  isufil2  23844  cfinufil  23864  flimopn  23911  fbflim2  23913  flfneii  23928  cnpflf  23937  fclssscls  23954  fclsnei  23955  fclsrest  23960  flimfnfcls  23964  fclscmp  23966  isfcf  23970  fcfnei  23971  alexsubALTlem3  23985  alexsubALTlem4  23986  alexsubALT  23987  tsmsgsum  24075  tsmsres  24080  tsmsxplem1  24089  ustincl  24144  ustdiag  24145  ustinvel  24146  ustexhalf  24147  cfiluexsm  24226  psmet0  24245  prdsbl  24428  metss  24445  metcnp3  24477  isngp4  24549  nmoi  24665  mulc1cncf  24847  cncfco  24849  lebnumii  24914  iscfil3  25223  iscau2  25227  iscau4  25229  equivcfil  25249  equivcau  25250  lmcau  25263  ismbf  25579  ellimc3  25830  lhop1  25969  dvfsumlem4  25986  dvfsum2  25991  dgrco  26231  fta1  26266  aalioulem2  26291  aalioulem4  26293  ulmclm  26346  ulmshftlem  26348  ulmcaulem  26353  ulmcau  26354  ulmcn  26358  cxploglim  26938  ftalem3  27035  chtub  27173  dchrelbasd  27200  2sqlem6  27384  2sqlem10  27389  dchrisumlema  27449  dchrisumlem2  27451  dchrisumlem3  27452  dchrvmasumlem2  27459  pntpbnd1  27547  pntibnd  27554  pntleml  27572  nolt02o  27657  noresle  27659  nosupbnd1lem1  27670  nosupbnd1lem4  27673  nosupbnd2lem1  27677  nosupbnd2  27678  nocvxminlem  27739  madebdaylemold  27853  n0subs  28277  brbtwn2  28830  colinearalg  28835  axcontlem4  28892  usgruspgrb  29108  cusgredg  29349  cusgrres  29374  usgredgsscusgredg  29385  fusgrn0degnn0  29425  wlk1walk  29565  wlkres  29596  wlkp1lem6  29604  wlkdlem2  29609  upgrwlkdvdelem  29664  pthdlem2lem  29695  lfgrn1cycl  29733  wwlksnredwwlkn  29823  wwlksnextproplem2  29838  clwwlkccatlem  29916  clwlkclwwlkf1lem3  29933  clwwisshclwwslemlem  29940  clwwlkf1  29976  clwwlkext2edg  29983  3cyclfrgrrn1  30212  n4cyclfrgr  30218  frgrwopregasn  30243  frgrwopregbsn  30244  isgrpo  30424  blocnilem  30731  ip2eqi  30783  htthlem  30844  hial0  31029  hial02  31030  hial2eq  31033  ocorth  31218  h1de2i  31480  pjjsi  31627  lnopunilem1  31937  lnophmlem1  31943  nmcexi  31953  riesz4i  31990  mdi  32222  mdbr3  32224  mdbr4  32225  dmdi  32229  dmdbr3  32232  dmdbr4  32233  dmdi4  32234  mdslmd1i  32256  atss  32273  atom1d  32280  atmd  32326  sumdmdlem2  32346  cdj1i  32360  cdj3i  32368  fnpreimac  32595  nn0min  32745  archiabllem1a  33135  archiabllem2a  33138  archiabl  33142  isarchiofld  33285  crefi  33824  pcmplfin  33837  fmcncfil  33908  sigaclcu  34094  unelsiga  34111  sigapildsys  34139  ldgenpisys  34143  measvun  34186  carsgclctunlem2  34297  sibfima  34316  fnrelpredd  35066  pfxwlk  35092  derangenlem  35139  subfacp1lem6  35153  resconn  35214  cvmcov  35231  cvmliftlem3  35255  cvmliftphtlem  35285  satfdmfmla  35368  mclsax  35537  dfon2lem6  35752  fwddifnp1  36129  opnrebl2  36285  nn0prpwlem  36286  nn0prpw  36287  neibastop2lem  36324  neibastop2  36325  filnetlem4  36345  bj-mooreset  37066  bj-ismoored0  37070  dfgcd3  37288  fin2so  37577  poimirlem25  37615  poimirlem29  37619  poimir  37623  mbfresfi  37636  ftc1cnnclem  37661  seqpo  37717  incsequz  37718  mettrifi  37727  geomcau  37729  caushft  37731  sstotbnd2  37744  equivtotbnd  37748  totbndbnd  37759  ismtybndlem  37776  heibor1lem  37779  bfplem2  37793  opidonOLD  37822  exidu1  37826  rngoideu  37873  isdrngo2  37928  unichnidl  38001  lsat0cv  38997  lcvexchlem4  39001  lcvexchlem5  39002  eqlkr3  39065  lub0N  39153  glb0N  39157  cvrnbtwn  39235  ltrneq2  40113  trlval2  40128  lpolsatN  41453  lpolpolsatN  41454  hdmap14lem12  41844  fsuppind  42560  nna4b4nsq  42630  incssnn0  42681  lnmlssfg  43051  unxpwdom3  43066  neik0pk1imk0  44018  ismnushort  44273  fnchoice  45001  monoordxrv  45456  monoord2xrv  45458  limcrecl  45606  fourierdlem54  46137  fourierdlem103  46186  fourierdlem104  46187  euoreqb  47086  smonoord  47333  iccpartlt  47386  iccpartgt  47389  iccpartdisj  47399  paireqne  47473  fmtnodvds  47506  perfectALTVlem2  47684  sbgoldbwt  47739  sbgoldbst  47740  sgoldbeven3prm  47745  mogoldbb  47747  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  bgoldbnnsum3prm  47766  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbndlem4  47770  bgoldbtbnd  47771  tgblthelfgott  47777  tgoldbach  47779  grimuhgr  47848  grimcnv  47849  grimco  47850  uhgrimedgi  47851  isuspgrim0  47855  upgrimwlklem5  47862  uhgrimisgrgriclem  47891  clnbgrgrimlem  47894  clnbgrgrim  47895  grimedg  47896  uspgrlimlem3  47950  uspgrlimlem4  47951  grlimgrtrilem2  47955  grlimgrtri  47956  grilcbri2  47964  grlicsym  47966  grlictr  47968  clnbgr3stgrgrlic  47972  lcosslsp  48362  linindslinci  48372  lindslinindsimp1  48381  ldepsnlinclem1  48429  ldepsnlinclem2  48430  iscnrm3r  48870  termc2  49351