Theorem rspcv 3631

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068

This theorem is referenced by:  rspccv  3632  rspcva  3633  rspccva  3634  rspcdva  3636  rspc2v  3646  rspc3v  3651  rspc4v  3655  rr19.3v  3680  rr19.28v  3681  rspsbc  3901  rspc2vd  3972  intmin  4992  ralxfrALT  5433  somo  5646  fr2nr  5677  weniso  7390  fr3nr  7807  limuni3  7889  tfinds  7897  funcnvuni  7972  poseq  8199  soseq  8200  suppfnss  8230  onnseq  8400  smo11  8420  tfrlem9  8441  tz7.49  8501  omeulem1  8638  oeordi  8643  naddelim  8742  nneneq  9272  nneneqOLD  9284  frfi  9349  unblem2  9357  unbnn2  9361  xpfiOLD  9387  ordiso2  9584  cantnflem1  9758  ttrcltr  9785  ttrclss  9789  ttrclselem2  9795  frins3  9824  rankunb  9919  tcrank  9953  carduni  10050  dfac8alem  10098  alephinit  10164  aceq3lem  10189  dfac5  10198  dfac12r  10216  dfac12k  10217  pwsdompw  10272  cflm  10319  isf32lem1  10422  isf32lem2  10423  isf34lem4  10446  hsmexlem4  10498  axcc3  10507  domtriomlem  10511  axdc3lem2  10520  axdc4lem  10524  axcclem  10526  axdclem  10588  alephval2  10641  winainflem  10762  eltskm  10912  squeeze0  12198  lbreu  12245  nnsub  12337  ublbneg  12998  zmax  13010  zbtwnre  13011  xrub  13374  infmremnf  13405  infmrp1  13406  fzrevral  13669  axdc4uzlem  14034  faclbnd4lem4  14345  ccatalpha  14641  wrdind  14770  wrd2ind  14771  reuccatpfxs1lem  14794  recan  15385  cau3lem  15403  caubnd2  15406  climrlim2  15593  climshftlem  15620  rlimcld2  15624  subcn2  15641  isercoll  15716  climcau  15719  serf0  15729  iseralt  15733  isumrpcl  15891  clim2prod  15936  ntrivcvgfvn0  15947  sqrt2irr  16297  ndvdssub  16457  dfgcd2  16593  lcmf  16680  lcmfunsnlem1  16684  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  lcmfdvdsb  16690  coprmgcdb  16696  coprmdvds1  16699  coprmprod  16708  coprmproddvdslem  16709  nprm  16735  dvdsprm  16750  coprm  16758  pcmpt  16939  pcmptdvds  16941  pcfac  16946  prmpwdvds  16951  unbenlem  16955  vdwlem10  17037  vdwlem13  17040  vdwnnlem1  17042  prmdvdsprmop  17090  prmgaplem7  17104  catideu  17733  initoid  18068  termoid  18069  initoeu1  18078  termoeu1  18085  isdrs2  18376  lublecllem  18430  lubun  18585  lidrididd  18708  sgrp2rid2ex  18962  dfgrp2  19002  grpidinv2  19037  dfgrp3lem  19078  issubg4  19185  efgi  19761  efgi2  19767  dprdss  20073  srgrz  20234  srglz  20235  srgisid  20236  rrgeq0i  20721  isdomn4  20738  islmodd  20886  rmodislmod  20950  rmodislmodOLD  20951  islmhm2  21060  rnglidlmcl  21249  ip2eq  21694  mvrf1  22029  psdmul  22193  cply1mul  22321  isclo2  23117  cnpnei  23293  cncls  23303  lmss  23327  cnt0  23375  isnrm2  23387  isreg2  23406  tgcmp  23430  uncmp  23432  dfconn2  23448  1stcclb  23473  2ndcctbss  23484  comppfsc  23561  kgencn2  23586  ptpjpre1  23600  txlm  23677  kqfvima  23759  kqt0lem  23765  isr0  23766  nrmr0reg  23778  fgss2  23903  isufil2  23937  cfinufil  23957  flimopn  24004  fbflim2  24006  flfneii  24021  cnpflf  24030  fclssscls  24047  fclsnei  24048  fclsrest  24053  flimfnfcls  24057  fclscmp  24059  isfcf  24063  fcfnei  24064  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  tsmsgsum  24168  tsmsres  24173  tsmsxplem1  24182  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  cfiluexsm  24320  psmet0  24339  prdsbl  24525  metss  24542  metcnp3  24574  isngp4  24646  nmoi  24770  mulc1cncf  24950  cncfco  24952  lebnumii  25017  iscfil3  25326  iscau2  25330  iscau4  25332  equivcfil  25352  equivcau  25353  lmcau  25366  ismbf  25682  ellimc3  25934  lhop1  26073  dvfsumlem4  26090  dvfsum2  26095  dgrco  26335  fta1  26368  aalioulem2  26393  aalioulem4  26395  ulmclm  26448  ulmshftlem  26450  ulmcaulem  26455  ulmcau  26456  ulmcn  26460  cxploglim  27039  ftalem3  27136  chtub  27274  dchrelbasd  27301  2sqlem6  27485  2sqlem10  27490  dchrisumlema  27550  dchrisumlem2  27552  dchrisumlem3  27553  dchrvmasumlem2  27560  pntpbnd1  27648  pntibnd  27655  pntleml  27673  nolt02o  27758  noresle  27760  nosupbnd1lem1  27771  nosupbnd1lem4  27774  nosupbnd2lem1  27778  nosupbnd2  27779  nocvxminlem  27840  madebdaylemold  27954  n0subs  28378  brbtwn2  28938  colinearalg  28943  axcontlem4  29000  usgruspgrb  29218  cusgredg  29459  cusgrres  29484  usgredgsscusgredg  29495  fusgrn0degnn0  29535  wlk1walk  29675  wlkres  29706  wlkp1lem6  29714  wlkdlem2  29719  upgrwlkdvdelem  29772  pthdlem2lem  29803  lfgrn1cycl  29838  wwlksnredwwlkn  29928  wwlksnextproplem2  29943  clwwlkccatlem  30021  clwlkclwwlkf1lem3  30038  clwwisshclwwslemlem  30045  clwwlkf1  30081  clwwlkext2edg  30088  3cyclfrgrrn1  30317  n4cyclfrgr  30323  frgrwopregasn  30348  frgrwopregbsn  30349  isgrpo  30529  blocnilem  30836  ip2eqi  30888  htthlem  30949  hial0  31134  hial02  31135  hial2eq  31138  ocorth  31323  h1de2i  31585  pjjsi  31732  lnopunilem1  32042  lnophmlem1  32048  nmcexi  32058  riesz4i  32095  mdi  32327  mdbr3  32329  mdbr4  32330  dmdi  32334  dmdbr3  32337  dmdbr4  32338  dmdi4  32339  mdslmd1i  32361  atss  32378  atom1d  32385  atmd  32431  sumdmdlem2  32451  cdj1i  32465  cdj3i  32473  fnpreimac  32689  nn0min  32824  archiabllem1a  33171  archiabllem2a  33174  archiabl  33178  isarchiofld  33312  crefi  33793  pcmplfin  33806  fmcncfil  33877  sigaclcu  34081  unelsiga  34098  sigapildsys  34126  ldgenpisys  34130  measvun  34173  carsgclctunlem2  34284  sibfima  34303  fnrelpredd  35065  pfxwlk  35091  derangenlem  35139  subfacp1lem6  35153  resconn  35214  cvmcov  35231  cvmliftlem3  35255  cvmliftphtlem  35285  satfdmfmla  35368  mclsax  35537  dfon2lem6  35752  fwddifnp1  36129  opnrebl2  36287  nn0prpwlem  36288  nn0prpw  36289  neibastop2lem  36326  neibastop2  36327  filnetlem4  36347  bj-mooreset  37068  bj-ismoored0  37072  dfgcd3  37290  fin2so  37567  poimirlem25  37605  poimirlem29  37609  poimir  37613  mbfresfi  37626  ftc1cnnclem  37651  seqpo  37707  incsequz  37708  mettrifi  37717  geomcau  37719  caushft  37721  sstotbnd2  37734  equivtotbnd  37738  totbndbnd  37749  ismtybndlem  37766  heibor1lem  37769  bfplem2  37783  opidonOLD  37812  exidu1  37816  rngoideu  37863  isdrngo2  37918  unichnidl  37991  lsat0cv  38989  lcvexchlem4  38993  lcvexchlem5  38994  eqlkr3  39057  lub0N  39145  glb0N  39149  cvrnbtwn  39227  ltrneq2  40105  trlval2  40120  lpolsatN  41445  lpolpolsatN  41446  hdmap14lem12  41836  fsuppind  42545  nna4b4nsq  42615  incssnn0  42667  lnmlssfg  43037  unxpwdom3  43052  neik0pk1imk0  44009  ismnushort  44270  fnchoice  44929  monoordxrv  45397  monoord2xrv  45399  limcrecl  45550  fourierdlem54  46081  fourierdlem103  46130  fourierdlem104  46131  euoreqb  47024  smonoord  47245  iccpartlt  47298  iccpartgt  47301  iccpartdisj  47311  paireqne  47385  fmtnodvds  47418  perfectALTVlem2  47596  sbgoldbwt  47651  sbgoldbst  47652  sgoldbeven3prm  47657  mogoldbb  47659  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  bgoldbnnsum3prm  47678  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  tgblthelfgott  47689  tgoldbach  47691  isuspgrim0  47756  grimuhgr  47762  grimcnv  47763  grimco  47764  uhgrimisgrgriclem  47782  clnbgrgrimlem  47785  clnbgrgrim  47786  grimedg  47787  uspgrlimlem3  47814  uspgrlimlem4  47815  grlimgrtrilem2  47819  grlimgrtri  47820  grilcbri2  47828  grlicsym  47830  grlictr  47832  lcosslsp  48167  linindslinci  48177  lindslinindsimp1  48186  ldepsnlinclem1  48234  ldepsnlinclem2  48235  iscnrm3r  48628