Theorem rspcv 3572

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

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

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  rspccv  3573  rspcva  3574  rspccva  3575  rspcdva  3577  rspc2v  3587  rspc3v  3592  rspc4v  3596  rr19.3v  3621  rr19.28v  3622  rspsbc  3826  rspc2vd  3895  intmin  4928  ralxfrALT  5380  somo  5602  fr2nr  5632  weniso  7357  fr3nr  7771  limuni3  7848  tfinds  7856  funcnvuni  7929  resf1extb  7931  poseq  8156  soseq  8157  suppfnss  8187  onnseq  8333  smo11  8353  tfrlem9  8374  tz7.49  8434  omeulem1  8569  oeordi  8575  naddelim  8675  nneneq  9200  frfi  9255  unblem2  9263  unbnn2  9267  ordiso2  9487  cantnflem1  9668  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  frins3  9737  rankunb  9832  tcrank  9866  scottex  9872  carduni  9986  dfac8alem  10032  alephinit  10098  aceq3lem  10123  dfac5  10131  dfac12r  10149  dfac12k  10150  pwsdompw  10205  cflm  10251  isf32lem1  10355  isf32lem2  10356  isf34lem4  10379  hsmexlem4  10431  axcc3  10440  domtriomlem  10444  axdc3lem2  10453  axdc4lem  10457  axcclem  10459  axdclem  10521  alephval2  10581  winainflem  10702  eltskm  10852  squeeze0  12142  lbreu  12189  nnsub  12304  ublbneg  12982  zmax  12994  zbtwnre  12995  xrub  13364  infmremnf  13396  infmrp1  13397  fzrevral  13667  axdc4uzlem  14047  faclbnd4lem4  14360  ccatalpha  14660  wrdind  14791  wrd2ind  14792  reuccatpfxs1lem  14815  recan  15424  cau3lem  15442  caubnd2  15445  climrlim2  15634  climshftlem  15661  rlimcld2  15665  subcn2  15682  isercoll  15755  climcau  15758  serf0  15768  iseralt  15772  isumrpcl  15932  clim2prod  15977  ntrivcvgfvn0  15988  sqrt2irr  16337  ndvdssub  16499  dfgcd2  16636  lcmf  16723  lcmfunsnlem1  16727  lcmfunsnlem2lem1  16728  lcmfunsnlem2lem2  16729  lcmfdvdsb  16733  coprmgcdb  16739  coprmdvds1  16742  coprmprod  16751  coprmproddvdslem  16752  nprm  16778  dvdsprm  16794  coprm  16802  pcmpt  16984  pcmptdvds  16986  pcfac  16991  prmpwdvds  16996  unbenlem  17000  vdwlem10  17082  vdwlem13  17085  vdwnnlem1  17087  prmdvdsprmop  17135  prmgaplem7  17149  catideu  17763  initoid  18090  termoid  18091  initoeu1  18100  termoeu1  18107  isdrs2  18394  lublecllem  18446  lubun  18603  lidrididd  18764  mgmidpfod  18770  sgrp2rid2ex  19039  dfgrp2  19086  grpidinv2  19121  dfgrp3lem  19161  issubg4  19269  efgi  19846  efgi2  19852  dprdss  20158  srgrz  20346  srglz  20347  srgisid  20348  rrgeq0i  20861  isdomn4  20877  isdrng3lem2  20915  islmodd  21050  rmodislmod  21114  islmhm2  21222  rnglidlmcl  21404  ip2eq  21866  mvrf1  22200  psdmul  22394  cply1mul  22521  isclo2  23313  cnpnei  23489  cncls  23499  lmss  23523  cnt0  23571  isnrm2  23583  isreg2  23602  tgcmp  23626  uncmp  23628  dfconn2  23644  1stcclb  23669  2ndcctbss  23681  comppfsc  23758  kgencn2  23783  ptpjpre1  23797  txlm  23874  kqfvima  23956  kqt0lem  23962  isr0  23963  nrmr0reg  23975  fgss2  24100  isufil2  24134  cfinufil  24154  flimopn  24201  fbflim2  24203  flfneii  24218  cnpflf  24227  fclssscls  24244  fclsnei  24245  fclsrest  24250  flimfnfcls  24254  fclscmp  24256  isfcf  24260  fcfnei  24261  alexsubALTlem3  24275  alexsubALTlem4  24276  alexsubALT  24277  tsmsgsum  24365  tsmsres  24370  tsmsxplem1  24379  ustincl  24434  ustdiag  24435  ustinvel  24436  ustexhalf  24437  cfiluexsm  24515  psmet0  24534  prdsbl  24717  metss  24734  metcnp3  24766  isngp4  24838  nmoi  24954  mulc1cncf  25133  cncfco  25135  lebnumii  25194  iscfil3  25501  iscau2  25505  iscau4  25507  equivcfil  25527  equivcau  25528  lmcau  25541  ismbf  25856  ellimc3  26106  lhop1  26241  dvfsumlem4  26256  dvfsum2  26261  dgrco  26501  fta1  26538  plyconz  26540  aalioulem2  26569  aalioulem4  26571  ulmclm  26623  ulmshftlem  26625  ulmcaulem  26630  ulmcau  26631  ulmcn  26635  cxploglim  27214  ftalem3  27311  chtub  27448  dchrelbasd  27475  2sqlem6  27659  2sqlem10  27664  dchrisumlema  27724  dchrisumlem2  27726  dchrisumlem3  27727  dchrvmasumlem2  27734  pntpbnd1  27822  pntibnd  27829  pntleml  27847  nolt02o  27931  noresle  27933  nosupbnd1lem1  27944  nosupbnd1lem4  27947  nosupbnd2lem1  27951  nosupbnd2  27952  nocvxminlem  28019  madebdaylemold  28163  n0subs  28628  z12zsodd  28747  brbtwn2  29362  colinearalg  29367  axcontlem4  29424  usgruspgrb  29643  cusgredg  29884  cusgrres  29908  usgredgsscusgredg  29919  fusgrn0degnn0  29959  wlk1walk  30098  wlkres  30128  wlkp1lem6  30136  wlkdlem2  30141  pfxwlk  30145  upgrwlkdvdelem  30201  pthdlem2lem  30232  lfgrn1cycl  30273  wwlksnredwwlkn  30363  wwlksnextproplem2  30378  clwwlkccatlem  30459  clwlkclwwlkf1lem3  30476  clwwisshclwwslemlem  30483  clwwlkf1  30519  clwwlkext2edg  30526  3cyclfrgrrn1  30765  n4cyclfrgr  30771  frgrwopregasn  30796  frgrwopregbsn  30797  isgrpo  30978  blocnilem  31285  ip2eqi  31337  htthlem  31398  hial0  31583  hial02  31584  hial2eq  31587  ocorth  31772  h1de2i  32034  pjjsi  32181  lnopunilem1  32491  lnophmlem1  32497  nmcexi  32507  riesz4i  32544  mdi  32776  mdbr3  32778  mdbr4  32779  dmdi  32783  dmdbr3  32786  dmdbr4  32787  dmdi4  32788  mdslmd1i  32810  atss  32827  atom1d  32834  atmd  32880  sumdmdlem2  32900  cdj1i  32914  cdj3i  32922  fnpreimac  33143  nn0min  33291  archiabllem1a  33631  archiabllem2a  33634  archiabl  33638  isarchiofld  33639  trisecnconstr  34302  crefi  34357  pcmplfin  34370  fmcncfil  34441  sigaclcu  34627  unelsiga  34644  sigapildsys  34673  ldgenpisys  34677  measvun  34720  carsgclctunlem2  34830  sibfima  34849  fnrelpredd  35596  fineqvnttrclse  35650  fineqvinfep  35651  derangenlem  35750  subfacp1lem6  35764  resconn  35825  cvmcov  35842  cvmliftlem3  35866  cvmliftphtlem  35896  satfdmfmla  35979  mclsax  36148  dfon2lem6  36365  fwddifnp1  36745  opnrebl2  36940  nn0prpwlem  36941  nn0prpw  36942  neibastop2lem  36979  neibastop2  36980  filnetlem4  37000  dfttc4  37149  bj-mooreset  37852  bj-ismoored0  37856  dfgcd3  38076  fin2so  38361  poimirlem25  38394  poimirlem29  38398  poimir  38402  mbfresfi  38415  ftc1cnnclem  38440  seqpo  38497  incsequz  38498  mettrifi  38507  geomcau  38509  caushft  38511  sstotbnd2  38524  equivtotbnd  38528  totbndbnd  38539  ismtybndlem  38556  heibor1lem  38559  bfplem2  38573  opidonOLD  38602  exidu1  38606  rngoideu  38653  isdrngo2  38708  unichnidl  38781  lsat0cv  39906  lcvexchlem4  39910  lcvexchlem5  39911  eqlkr3  39974  lub0N  40062  glb0N  40066  cvrnbtwn  40144  ltrneq2  41021  trlval2  41036  lpolsatN  42361  lpolpolsatN  42362  hdmap14lem12  42752  fsuppind  43436  nna4b4nsq  43506  incssnn0  43556  lnmlssfg  43921  unxpwdom3  43936  neik0pk1imk0  44887  ismnushort  45125  fnchoice  45863  monoordxrv  46309  monoord2xrv  46311  limcrecl  46459  fourierdlem54  46988  fourierdlem103  47037  fourierdlem104  47038  euoreqb  47997  smonoord  48265  iccpartlt  48324  iccpartgt  48327  iccpartdisj  48337  paireqne  48411  fmtnodvds  48447  perfectALTVlem2  48638  sbgoldbwt  48693  sbgoldbst  48694  sgoldbeven3prm  48699  mogoldbb  48701  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  bgoldbnnsum3prm  48720  bgoldbtbndlem2  48722  bgoldbtbndlem3  48723  bgoldbtbndlem4  48724  bgoldbtbnd  48725  tgblthelfgott  48731  tgoldbach  48733  grimuhgr  48803  grimcnv  48804  grimco  48805  uhgrimedgi  48806  isuspgrim0  48810  upgrimwlklem5  48817  uhgrimisgrgriclem  48846  clnbgrgrimlem  48849  clnbgrgrim  48850  grimedg  48851  uspgrlimlem3  48906  uspgrlimlem4  48907  grlimedgclnbgr  48911  grlimgrtrilem2  48918  grlimgrtri  48919  grilcbri2  48927  grlicsym  48929  grlictr  48931  clnbgr3stgrgrlim  48935  clnbgr3stgrgrlic  48936  lcosslsp  49368  linindslinci  49378  lindslinindsimp1  49387  ldepsnlinclem1  49435  ldepsnlinclem2  49436  iscnrm3r  49874  initc  50017  termc2  50444  nellindf  50803