Theorem rspcv 3576

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081

This theorem is used by:  rspccv  3577  rspcva  3578  rspccva  3579  rspcdva  3581  rspc2v  3590  rspc3v  3595  rspc4v  3599  rr19.3v  3624  rr19.28v  3625  rspsbc  3830  rspc2vd  3899  intmin  4933  ralxfrALT  5384  somo  5605  fr2nr  5635  weniso  7395  fr3nr  7818  limuni3  7897  tfinds  7905  funcnvuni  7978  resf1extb  7980  poseq  8212  soseq  8213  suppfnss  8244  onnseq  8390  smo11  8410  tfrlem9  8431  tz7.49  8493  omeulem1  8628  oeordi  8634  naddelim  8734  nneneq  9259  frfi  9314  unblem2  9323  unbnn2  9327  ordiso2  9546  cantnflem1  9727  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  frins3  9796  rankunb  9901  tcrank  9938  scottex  9970  carduni  10101  dfac8alem  10147  alephinit  10213  aceq3lem  10238  dfac5  10246  dfac12r  10264  dfac12k  10265  pwsdompw  10320  cflm  10366  isf32lem1  10470  isf32lem2  10471  isf34lem4  10494  hsmexlem4  10546  axcc3  10555  domtriomlem  10559  axdc3lem2  10568  axdc4lem  10572  axcclem  10574  axdclem  10636  alephval2  10696  winainflem  10817  eltskm  10967  squeeze0  12260  lbreu  12307  nnsub  12422  ublbneg  13100  zmax  13112  zbtwnre  13113  xrub  13482  infmremnf  13514  infmrp1  13515  fzrevral  13786  axdc4uzlem  14166  faclbnd4lem4  14481  ccatalpha  14781  wrdind  14913  wrd2ind  14914  reuccatpfxs1lem  14937  recan  15547  cau3lem  15566  caubnd2  15569  climrlim2  15758  climshftlem  15785  rlimcld2  15789  subcn2  15806  isercoll  15879  climcau  15882  serf0  15892  iseralt  15896  isumrpcl  16056  clim2prod  16101  ntrivcvgfvn0  16112  sqrt2irr  16461  ndvdssub  16623  dfgcd2  16763  lcmf  16852  lcmfunsnlem1  16856  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  lcmfdvdsb  16862  coprmgcdb  16868  coprmdvds1  16871  coprmprod  16880  coprmproddvdslem  16881  nprm  16907  dvdsprm  16923  coprm  16931  pcmpt  17114  pcmptdvds  17116  pcfac  17121  prmpwdvds  17126  unbenlem  17130  vdwlem10  17212  vdwlem13  17215  vdwnnlem1  17217  prmdvdsprmop  17265  prmgaplem7  17279  catideu  17899  initoid  18226  termoid  18227  initoeu1  18236  termoeu1  18243  isdrs2  18530  lublecllem  18582  lubun  18739  lidrididd  18901  mgmidpfod  18907  sgrp2rid2ex  19176  dfgrp2  19223  grpidinv2  19258  dfgrp3lem  19298  issubg4  19406  efgi  19984  efgi2  19990  dprdss  20296  srgrz  20484  srglz  20485  srgisid  20486  rrgeq0i  21002  isdomn4  21018  isdrng3lem2  21057  islmodd  21192  rmodislmod  21256  islmhm2  21364  rnglidlmcl  21546  ip2eq  22014  mvrf1  22348  psdmul  22542  cply1mul  22669  isclo2  23461  cnpnei  23637  cncls  23647  lmss  23671  cnt0  23719  isnrm2  23731  isreg2  23750  tgcmp  23774  uncmp  23776  dfconn2  23792  1stcclb  23817  2ndcctbss  23829  comppfsc  23906  kgencn2  23931  ptpjpre1  23945  txlm  24022  kqfvima  24104  kqt0lem  24110  isr0  24111  nrmr0reg  24123  fgss2  24248  isufil2  24282  cfinufil  24302  flimopn  24349  fbflim2  24351  flfneii  24366  cnpflf  24375  fclssscls  24392  fclsnei  24393  fclsrest  24398  flimfnfcls  24402  fclscmp  24404  isfcf  24408  fcfnei  24409  alexsubALTlem3  24423  alexsubALTlem4  24424  alexsubALT  24425  tsmsgsum  24513  tsmsres  24518  tsmsxplem1  24527  ustincl  24582  ustdiag  24583  ustinvel  24584  ustexhalf  24585  cfiluexsm  24663  psmet0  24682  prdsbl  24865  metss  24882  metcnp3  24914  isngp4  24986  nmoi  25102  mulc1cncf  25281  cncfco  25283  lebnumii  25342  iscfil3  25649  iscau2  25653  iscau4  25655  equivcfil  25675  equivcau  25676  lmcau  25689  ismbf  26004  ellimc3  26254  lhop1  26389  dvfsumlem4  26404  dvfsum2  26409  dgrco  26649  fta1  26684  plyconz  26686  aalioulem2  26717  aalioulem4  26719  ulmclm  26771  ulmshftlem  26773  ulmcaulem  26778  ulmcau  26779  ulmcn  26783  cxploglim  27362  ftalem3  27459  chtub  27596  dchrelbasd  27623  2sqlem6  27807  2sqlem10  27812  dchrisumlema  27872  dchrisumlem2  27874  dchrisumlem3  27875  dchrvmasumlem2  27882  pntpbnd1  27970  pntibnd  27977  pntleml  27995  fltoprm  28052  nolt02o  28109  noresle  28111  nosupbnd1lem1  28122  nosupbnd1lem4  28125  nosupbnd2lem1  28129  nosupbnd2  28130  nocvxminlem  28197  madebdaylemold  28341  n0subs  28806  z12zsodd  28925  brbtwn2  29540  colinearalg  29545  axcontlem4  29602  usgruspgrb  29821  cusgredg  30062  cusgrres  30086  usgredgsscusgredg  30097  fusgrn0degnn0  30137  wlk1walk  30276  wlkres  30306  wlkp1lem6  30314  wlkdlem2  30319  pfxwlk  30323  upgrwlkdvdelem  30379  pthdlem2lem  30410  lfgrn1cycl  30451  wwlksnredwwlkn  30541  wwlksnextproplem2  30556  clwwlkccatlem  30637  clwlkclwwlkf1lem3  30654  clwwisshclwwslemlem  30661  clwwlkf1  30697  clwwlkext2edg  30704  3cyclfrgrrn1  30943  n4cyclfrgr  30949  frgrwopregasn  30974  frgrwopregbsn  30975  isgrpo  31156  blocnilem  31463  ip2eqi  31515  htthlem  31576  hial0  31761  hial02  31762  hial2eq  31765  ocorth  31950  h1de2i  32212  pjjsi  32359  lnopunilem1  32669  lnophmlem1  32675  nmcexi  32685  riesz4i  32722  mdi  32954  mdbr3  32956  mdbr4  32957  dmdi  32961  dmdbr3  32964  dmdbr4  32965  dmdi4  32966  mdslmd1i  32988  atss  33005  atom1d  33012  atmd  33058  sumdmdlem2  33078  cdj1i  33092  cdj3i  33100  fnpreimac  33362  nn0min  33508  archiabllem1a  33851  archiabllem2a  33854  archiabl  33858  isarchiofld  33859  trisecnconstr  34535  crefi  34590  pcmplfin  34603  fmcncfil  34674  sigaclcu  34860  unelsiga  34877  sigapildsys  34906  ldgenpisys  34910  measvun  34953  carsgclctunlem2  35062  sibfima  35081  fnrelpredd  35845  0elscott  35878  fineqvnttrclse  35933  fineqvinfep  35934  onprcf1acwevdlem2  36087  derangenlem  36144  subfacp1lem6  36158  resconn  36219  cvmcov  36236  cvmliftlem3  36260  cvmliftphtlem  36290  satfdmfmla  36373  mclsax  36542  mirimanoffr  36668  mirimanofffr  36670  dfon2lem6  36765  fwddifnp1  37145  opnrebl2  37324  nn0prpwlem  37325  nn0prpw  37326  neibastop2lem  37363  neibastop2  37364  filnetlem4  37384  dfttc4  37533  bj-mooreset  38293  bj-ismoored0  38297  dfgcd3  38513  fin2so  38798  poimirlem25  38831  poimirlem29  38835  poimir  38839  mbfresfi  38852  ftc1cnnclem  38877  seqpo  38947  incsequz  38948  mettrifi  38957  geomcau  38959  caushft  38961  sstotbnd2  38974  equivtotbnd  38978  totbndbnd  38989  ismtybndlem  39006  heibor1lem  39009  bfplem2  39023  opidonOLD  39052  exidu1  39056  rngoideu  39103  isdrngo2  39158  unichnidl  39231  lsat0cv  40356  lcvexchlem4  40360  lcvexchlem5  40361  eqlkr3  40424  lub0N  40512  glb0N  40516  cvrnbtwn  40594  ltrneq2  41471  trlval2  41486  lpolsatN  42811  lpolpolsatN  42812  hdmap14lem12  43202  fsuppind  43884  incssnn0  43988  lnmlssfg  44348  unxpwdom3  44363  neik0pk1imk0  45308  ismnushort  45546  fnchoice  46320  monoordxrv  46764  monoord2xrv  46766  limcrecl  46914  fourierdlem54  47443  fourierdlem103  47492  fourierdlem104  47493  euoreqb  48453  smonoord  48720  iccpartlt  48779  iccpartgt  48782  iccpartdisj  48792  paireqne  48866  fmtnodvds  48902  perfectALTVlem2  49093  sbgoldbwt  49148  sbgoldbst  49149  sgoldbeven3prm  49154  mogoldbb  49156  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  bgoldbnnsum3prm  49175  bgoldbtbndlem2  49177  bgoldbtbndlem3  49178  bgoldbtbndlem4  49179  bgoldbtbnd  49180  tgblthelfgott  49186  tgoldbach  49188  grimuhgr  49258  grimcnv  49259  grimco  49260  uhgrimedgi  49261  isuspgrim0  49265  upgrimwlklem5  49272  uhgrimisgrgriclem  49301  clnbgrgrimlem  49304  clnbgrgrim  49305  grimedg  49306  uspgrlimlem3  49361  uspgrlimlem4  49362  grlimedgclnbgr  49366  grlimgrtrilem2  49373  grlimgrtri  49374  grilcbri2  49382  grlicsym  49384  grlictr  49386  clnbgr3stgrgrlim  49390  clnbgr3stgrgrlic  49391  lcosslsp  49881  linindslinci  49891  lindslinindsimp1  49900  ldepsnlinclem1  49948  ldepsnlinclem2  49949  iscnrm3r  50393  initc  50537  termc2  50984  nellindf  51398