Theorem rspcv 3560

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  rspccv  3561  rspcva  3562  rspccva  3563  rspcdva  3565  rspc2v  3575  rspc3v  3580  rspc4v  3584  rr19.3v  3609  rr19.28v  3610  rspsbc  3817  rspc2vd  3885  intmin  4910  ralxfrALT  5357  somo  5578  fr2nr  5608  weniso  7309  fr3nr  7726  limuni3  7803  tfinds  7811  funcnvuni  7883  resf1extb  7885  poseq  8108  soseq  8109  suppfnss  8139  onnseq  8284  smo11  8304  tfrlem9  8324  tz7.49  8384  omeulem1  8517  oeordi  8523  naddelim  8622  nneneq  9140  frfi  9195  unblem2  9203  unbnn2  9207  ordiso2  9430  cantnflem1  9610  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  frins3  9679  rankunb  9774  tcrank  9808  carduni  9905  dfac8alem  9951  alephinit  10017  aceq3lem  10042  dfac5  10051  dfac12r  10069  dfac12k  10070  pwsdompw  10125  cflm  10172  isf32lem1  10275  isf32lem2  10276  isf34lem4  10299  hsmexlem4  10351  axcc3  10360  domtriomlem  10364  axdc3lem2  10373  axdc4lem  10377  axcclem  10379  axdclem  10441  alephval2  10495  winainflem  10616  eltskm  10766  squeeze0  12059  lbreu  12106  nnsub  12221  ublbneg  12883  zmax  12895  zbtwnre  12896  xrub  13264  infmremnf  13296  infmrp1  13297  fzrevral  13566  axdc4uzlem  13945  faclbnd4lem4  14258  ccatalpha  14556  wrdind  14684  wrd2ind  14685  reuccatpfxs1lem  14708  recan  15299  cau3lem  15317  caubnd2  15320  climrlim2  15509  climshftlem  15536  rlimcld2  15540  subcn2  15557  isercoll  15630  climcau  15633  serf0  15643  iseralt  15647  isumrpcl  15808  clim2prod  15853  ntrivcvgfvn0  15864  sqrt2irr  16216  ndvdssub  16378  dfgcd2  16515  lcmf  16602  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfdvdsb  16612  coprmgcdb  16618  coprmdvds1  16621  coprmprod  16630  coprmproddvdslem  16631  nprm  16657  dvdsprm  16673  coprm  16681  pcmpt  16863  pcmptdvds  16865  pcfac  16870  prmpwdvds  16875  unbenlem  16879  vdwlem10  16961  vdwlem13  16964  vdwnnlem1  16966  prmdvdsprmop  17014  prmgaplem7  17028  catideu  17641  initoid  17968  termoid  17969  initoeu1  17978  termoeu1  17985  isdrs2  18272  lublecllem  18324  lubun  18481  lidrididd  18638  sgrp2rid2ex  18898  dfgrp2  18938  grpidinv2  18973  dfgrp3lem  19014  issubg4  19121  efgi  19694  efgi2  19700  dprdss  20006  srgrz  20188  srglz  20189  srgisid  20190  rrgeq0i  20676  isdomn4  20693  islmodd  20861  rmodislmod  20925  islmhm2  21033  rnglidlmcl  21214  ip2eq  21633  mvrf1  21964  psdmul  22132  cply1mul  22261  isclo2  23053  cnpnei  23229  cncls  23239  lmss  23263  cnt0  23311  isnrm2  23323  isreg2  23342  tgcmp  23366  uncmp  23368  dfconn2  23384  1stcclb  23409  2ndcctbss  23420  comppfsc  23497  kgencn2  23522  ptpjpre1  23536  txlm  23613  kqfvima  23695  kqt0lem  23701  isr0  23702  nrmr0reg  23714  fgss2  23839  isufil2  23873  cfinufil  23893  flimopn  23940  fbflim2  23942  flfneii  23957  cnpflf  23966  fclssscls  23983  fclsnei  23984  fclsrest  23989  flimfnfcls  23993  fclscmp  23995  isfcf  23999  fcfnei  24000  alexsubALTlem3  24014  alexsubALTlem4  24015  alexsubALT  24016  tsmsgsum  24104  tsmsres  24109  tsmsxplem1  24118  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  cfiluexsm  24254  psmet0  24273  prdsbl  24456  metss  24473  metcnp3  24505  isngp4  24577  nmoi  24693  mulc1cncf  24872  cncfco  24874  lebnumii  24933  iscfil3  25240  iscau2  25244  iscau4  25246  equivcfil  25266  equivcau  25267  lmcau  25280  ismbf  25595  ellimc3  25846  lhop1  25981  dvfsumlem4  25996  dvfsum2  26001  dgrco  26240  fta1  26274  aalioulem2  26299  aalioulem4  26301  ulmclm  26352  ulmshftlem  26354  ulmcaulem  26359  ulmcau  26360  ulmcn  26364  cxploglim  26941  ftalem3  27038  chtub  27175  dchrelbasd  27202  2sqlem6  27386  2sqlem10  27391  dchrisumlema  27451  dchrisumlem2  27453  dchrisumlem3  27454  dchrvmasumlem2  27461  pntpbnd1  27549  pntibnd  27556  pntleml  27574  nolt02o  27659  noresle  27661  nosupbnd1lem1  27672  nosupbnd1lem4  27675  nosupbnd2lem1  27679  nosupbnd2  27680  nocvxminlem  27746  madebdaylemold  27890  n0subs  28355  z12zsodd  28474  brbtwn2  28974  colinearalg  28979  axcontlem4  29036  usgruspgrb  29252  cusgredg  29493  cusgrres  29517  usgredgsscusgredg  29528  fusgrn0degnn0  29568  wlk1walk  29707  wlkres  29737  wlkp1lem6  29745  wlkdlem2  29750  upgrwlkdvdelem  29804  pthdlem2lem  29835  lfgrn1cycl  29873  wwlksnredwwlkn  29963  wwlksnextproplem2  29978  clwwlkccatlem  30059  clwlkclwwlkf1lem3  30076  clwwisshclwwslemlem  30083  clwwlkf1  30119  clwwlkext2edg  30126  3cyclfrgrrn1  30355  n4cyclfrgr  30361  frgrwopregasn  30386  frgrwopregbsn  30387  isgrpo  30568  blocnilem  30875  ip2eqi  30927  htthlem  30988  hial0  31173  hial02  31174  hial2eq  31177  ocorth  31362  h1de2i  31624  pjjsi  31771  lnopunilem1  32081  lnophmlem1  32087  nmcexi  32097  riesz4i  32134  mdi  32366  mdbr3  32368  mdbr4  32369  dmdi  32373  dmdbr3  32376  dmdbr4  32377  dmdi4  32378  mdslmd1i  32400  atss  32417  atom1d  32424  atmd  32470  sumdmdlem2  32490  cdj1i  32504  cdj3i  32512  fnpreimac  32743  nn0min  32894  archiabllem1a  33252  archiabllem2a  33255  archiabl  33259  isarchiofld  33260  trisecnconstr  33936  crefi  33991  pcmplfin  34004  fmcncfil  34075  sigaclcu  34261  unelsiga  34278  sigapildsys  34306  ldgenpisys  34310  measvun  34353  carsgclctunlem2  34463  sibfima  34482  fnrelpredd  35234  fineqvnttrclse  35268  fineqvinfep  35269  pfxwlk  35306  derangenlem  35353  subfacp1lem6  35367  resconn  35428  cvmcov  35445  cvmliftlem3  35469  cvmliftphtlem  35499  satfdmfmla  35582  mclsax  35751  dfon2lem6  35968  fwddifnp1  36347  opnrebl2  36503  nn0prpwlem  36504  nn0prpw  36505  neibastop2lem  36542  neibastop2  36543  filnetlem4  36563  dfttc4  36712  bj-mooreset  37414  bj-ismoored0  37418  dfgcd3  37638  fin2so  37928  poimirlem25  37966  poimirlem29  37970  poimir  37974  mbfresfi  37987  ftc1cnnclem  38012  seqpo  38068  incsequz  38069  mettrifi  38078  geomcau  38080  caushft  38082  sstotbnd2  38095  equivtotbnd  38099  totbndbnd  38110  ismtybndlem  38127  heibor1lem  38130  bfplem2  38144  opidonOLD  38173  exidu1  38177  rngoideu  38224  isdrngo2  38279  unichnidl  38352  lsat0cv  39479  lcvexchlem4  39483  lcvexchlem5  39484  eqlkr3  39547  lub0N  39635  glb0N  39639  cvrnbtwn  39717  ltrneq2  40594  trlval2  40609  lpolsatN  41934  lpolpolsatN  41935  hdmap14lem12  42325  fsuppind  43023  nna4b4nsq  43093  incssnn0  43143  lnmlssfg  43508  unxpwdom3  43523  neik0pk1imk0  44474  ismnushort  44728  fnchoice  45460  monoordxrv  45909  monoord2xrv  45911  limcrecl  46059  fourierdlem54  46588  fourierdlem103  46637  fourierdlem104  46638  euoreqb  47557  smonoord  47825  iccpartlt  47884  iccpartgt  47887  iccpartdisj  47897  paireqne  47971  fmtnodvds  48007  perfectALTVlem2  48198  sbgoldbwt  48253  sbgoldbst  48254  sgoldbeven3prm  48259  mogoldbb  48261  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  bgoldbnnsum3prm  48280  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbndlem4  48284  bgoldbtbnd  48285  tgblthelfgott  48291  tgoldbach  48293  grimuhgr  48363  grimcnv  48364  grimco  48365  uhgrimedgi  48366  isuspgrim0  48370  upgrimwlklem5  48377  uhgrimisgrgriclem  48406  clnbgrgrimlem  48409  clnbgrgrim  48410  grimedg  48411  uspgrlimlem3  48466  uspgrlimlem4  48467  grlimedgclnbgr  48471  grlimgrtrilem2  48478  grlimgrtri  48479  grilcbri2  48487  grlicsym  48489  grlictr  48491  clnbgr3stgrgrlim  48495  clnbgr3stgrgrlic  48496  lcosslsp  48914  linindslinci  48924  lindslinindsimp1  48933  ldepsnlinclem1  48981  ldepsnlinclem2  48982  iscnrm3r  49423  initc  49566  termc2  49993