Theorem rspcv 3609

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2138, ax-11 2155, ax-12 2172. (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 483	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcdv 3605	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063

This theorem is referenced by:  rspccv  3610  rspcva  3611  rspccva  3612  rspcdva  3614  rspc2v  3623  rspc3v  3628  rspc4v  3631  rr19.3v  3658  rr19.28v  3659  rspsbc  3874  rspc2vd  3945  intmin  4973  ralxfrALT  5414  somo  5626  fr2nr  5655  weniso  7351  fr3nr  7759  limuni3  7841  tfinds  7849  funcnvuni  7922  poseq  8144  soseq  8145  suppfnss  8174  onnseq  8344  smo11  8364  tfrlem9  8385  tz7.49  8445  omeulem1  8582  oeordi  8587  naddelim  8685  nneneq  9209  nneneqOLD  9221  frfi  9288  unblem2  9296  unbnn2  9300  xpfiOLD  9318  ordiso2  9510  cantnflem1  9684  ttrcltr  9711  ttrclss  9715  ttrclselem2  9721  frins3  9750  rankunb  9845  tcrank  9879  carduni  9976  dfac8alem  10024  alephinit  10090  aceq3lem  10115  dfac5  10123  dfac12r  10141  dfac12k  10142  pwsdompw  10199  cflm  10245  isf32lem1  10348  isf32lem2  10349  isf34lem4  10372  hsmexlem4  10424  axcc3  10433  domtriomlem  10437  axdc3lem2  10446  axdc4lem  10450  axcclem  10452  axdclem  10514  alephval2  10567  winainflem  10688  eltskm  10838  squeeze0  12117  lbreu  12164  nnsub  12256  ublbneg  12917  zmax  12929  zbtwnre  12930  xrub  13291  infmremnf  13322  infmrp1  13323  fzrevral  13586  axdc4uzlem  13948  faclbnd4lem4  14256  ccatalpha  14543  wrdind  14672  wrd2ind  14673  reuccatpfxs1lem  14696  recan  15283  cau3lem  15301  caubnd2  15304  climrlim2  15491  climshftlem  15518  rlimcld2  15522  subcn2  15539  isercoll  15614  climcau  15617  serf0  15627  iseralt  15631  isumrpcl  15789  clim2prod  15834  ntrivcvgfvn0  15845  sqrt2irr  16192  ndvdssub  16352  dfgcd2  16488  lcmf  16570  lcmfunsnlem1  16574  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  lcmfdvdsb  16580  coprmgcdb  16586  coprmdvds1  16589  coprmprod  16598  coprmproddvdslem  16599  nprm  16625  dvdsprm  16640  coprm  16648  pcmpt  16825  pcmptdvds  16827  pcfac  16832  prmpwdvds  16837  unbenlem  16841  vdwlem10  16923  vdwlem13  16926  vdwnnlem1  16928  prmdvdsprmop  16976  prmgaplem7  16990  catideu  17619  initoid  17951  termoid  17952  initoeu1  17961  termoeu1  17968  isdrs2  18259  lublecllem  18313  lubun  18468  lidrididd  18589  sgrp2rid2ex  18808  dfgrp2  18847  grpidinv2  18882  dfgrp3lem  18921  issubg4  19025  efgi  19587  efgi2  19593  dprdss  19899  srgrz  20030  srglz  20031  srgisid  20032  f1rhm0to0ALT  20280  islmodd  20477  rmodislmod  20540  rmodislmodOLD  20541  islmhm2  20649  rrgeq0i  20905  isdomn4  20918  ip2eq  21206  mvrf1  21545  cply1mul  21818  isclo2  22592  cnpnei  22768  cncls  22778  lmss  22802  cnt0  22850  isnrm2  22862  isreg2  22881  tgcmp  22905  uncmp  22907  dfconn2  22923  1stcclb  22948  2ndcctbss  22959  comppfsc  23036  kgencn2  23061  ptpjpre1  23075  txlm  23152  kqfvima  23234  kqt0lem  23240  isr0  23241  nrmr0reg  23253  fgss2  23378  isufil2  23412  cfinufil  23432  flimopn  23479  fbflim2  23481  flfneii  23496  cnpflf  23505  fclssscls  23522  fclsnei  23523  fclsrest  23528  flimfnfcls  23532  fclscmp  23534  isfcf  23538  fcfnei  23539  alexsubALTlem3  23553  alexsubALTlem4  23554  alexsubALT  23555  tsmsgsum  23643  tsmsres  23648  tsmsxplem1  23657  ustincl  23712  ustdiag  23713  ustinvel  23714  ustexhalf  23715  cfiluexsm  23795  psmet0  23814  prdsbl  24000  metss  24017  metcnp3  24049  isngp4  24121  nmoi  24245  mulc1cncf  24421  cncfco  24423  lebnumii  24482  iscfil3  24790  iscau2  24794  iscau4  24796  equivcfil  24816  equivcau  24817  lmcau  24830  ismbf  25145  ellimc3  25396  lhop1  25531  dvfsumlem4  25546  dvfsum2  25551  dgrco  25789  fta1  25821  aalioulem2  25846  aalioulem4  25848  ulmclm  25899  ulmshftlem  25901  ulmcaulem  25906  ulmcau  25907  ulmcn  25911  cxploglim  26482  ftalem3  26579  chtub  26715  dchrelbasd  26742  2sqlem6  26926  2sqlem10  26931  dchrisumlema  26991  dchrisumlem2  26993  dchrisumlem3  26994  dchrvmasumlem2  27001  pntpbnd1  27089  pntibnd  27096  pntleml  27114  nolt02o  27198  noresle  27200  nosupbnd1lem1  27211  nosupbnd1lem4  27214  nosupbnd2lem1  27218  nosupbnd2  27219  nocvxminlem  27279  madebdaylemold  27392  brbtwn2  28163  colinearalg  28168  axcontlem4  28225  usgruspgrb  28441  cusgredg  28681  cusgrres  28705  usgredgsscusgredg  28716  fusgrn0degnn0  28756  wlk1walk  28896  wlkres  28927  wlkp1lem6  28935  wlkdlem2  28940  upgrwlkdvdelem  28993  pthdlem2lem  29024  lfgrn1cycl  29059  wwlksnredwwlkn  29149  wwlksnextproplem2  29164  clwwlkccatlem  29242  clwlkclwwlkf1lem3  29259  clwwisshclwwslemlem  29266  clwwlkf1  29302  clwwlkext2edg  29309  3cyclfrgrrn1  29538  n4cyclfrgr  29544  frgrwopregasn  29569  frgrwopregbsn  29570  isgrpo  29750  blocnilem  30057  ip2eqi  30109  htthlem  30170  hial0  30355  hial02  30356  hial2eq  30359  ocorth  30544  h1de2i  30806  pjjsi  30953  lnopunilem1  31263  lnophmlem1  31269  nmcexi  31279  riesz4i  31316  mdi  31548  mdbr3  31550  mdbr4  31551  dmdi  31555  dmdbr3  31558  dmdbr4  31559  dmdi4  31560  mdslmd1i  31582  atss  31599  atom1d  31606  atmd  31652  sumdmdlem2  31672  cdj1i  31686  cdj3i  31694  fnpreimac  31896  nn0min  32026  archiabllem1a  32337  archiabllem2a  32340  archiabl  32344  isarchiofld  32435  crefi  32827  pcmplfin  32840  fmcncfil  32911  sigaclcu  33115  unelsiga  33132  sigapildsys  33160  ldgenpisys  33164  measvun  33207  carsgclctunlem2  33318  sibfima  33337  fnrelpredd  34092  pfxwlk  34114  derangenlem  34162  subfacp1lem6  34176  resconn  34237  cvmcov  34254  cvmliftlem3  34278  cvmliftphtlem  34308  satfdmfmla  34391  mclsax  34560  dfon2lem6  34760  fwddifnp1  35137  opnrebl2  35206  nn0prpwlem  35207  nn0prpw  35208  neibastop2lem  35245  neibastop2  35246  filnetlem4  35266  bj-mooreset  35983  bj-ismoored0  35987  dfgcd3  36205  fin2so  36475  poimirlem25  36513  poimirlem29  36517  poimir  36521  mbfresfi  36534  ftc1cnnclem  36559  seqpo  36615  incsequz  36616  mettrifi  36625  geomcau  36627  caushft  36629  sstotbnd2  36642  equivtotbnd  36646  totbndbnd  36657  ismtybndlem  36674  heibor1lem  36677  bfplem2  36691  opidonOLD  36720  exidu1  36724  rngoideu  36771  isdrngo2  36826  unichnidl  36899  lsat0cv  37903  lcvexchlem4  37907  lcvexchlem5  37908  eqlkr3  37971  lub0N  38059  glb0N  38063  cvrnbtwn  38141  ltrneq2  39019  trlval2  39034  lpolsatN  40359  lpolpolsatN  40360  hdmap14lem12  40750  fsuppind  41162  nna4b4nsq  41402  incssnn0  41449  lnmlssfg  41822  unxpwdom3  41837  neik0pk1imk0  42798  ismnushort  43060  fnchoice  43713  monoordxrv  44192  monoord2xrv  44194  limcrecl  44345  fourierdlem54  44876  fourierdlem103  44925  fourierdlem104  44926  euoreqb  45817  smonoord  46039  iccpartlt  46092  iccpartgt  46095  iccpartdisj  46105  paireqne  46179  fmtnodvds  46212  perfectALTVlem2  46390  sbgoldbwt  46445  sbgoldbst  46446  sgoldbeven3prm  46451  mogoldbb  46453  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  bgoldbnnsum3prm  46472  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbndlem4  46476  bgoldbtbnd  46477  tgblthelfgott  46483  tgoldbach  46485  isomuspgrlem2c  46498  isomuspgrlem2d  46499  rnglidlmcl  46748  lcosslsp  47119  linindslinci  47129  lindslinindsimp1  47138  ldepsnlinclem1  47186  ldepsnlinclem2  47187  iscnrm3r  47581