Theorem rspcv 3558

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 482	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcdv 3554	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

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

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070

This theorem is referenced by:  rspccv  3559  rspcva  3560  rspccva  3561  rspcdva  3563  rspc2v  3571  rspc3v  3574  rr19.3v  3599  rr19.28v  3600  rspsbc  3813  rspc2vd  3884  intmin  4900  ralxfrALT  5339  somo  5541  fr2nr  5568  weniso  7234  fr3nr  7631  limuni3  7708  tfinds  7715  funcnvuni  7787  suppfnss  8014  onnseq  8184  smo11  8204  tfrlem9  8225  tz7.49  8285  omeulem1  8422  oeordi  8427  nneneq  9001  nneneqOLD  9013  frfi  9068  unblem2  9076  unbnn2  9080  xpfi  9094  ordiso2  9283  cantnflem1  9456  ttrcltr  9483  ttrclss  9487  ttrclselem2  9493  frins3  9522  rankunb  9617  tcrank  9651  carduni  9748  dfac8alem  9794  alephinit  9860  aceq3lem  9885  dfac5  9893  dfac12r  9911  dfac12k  9912  pwsdompw  9969  cflm  10015  isf32lem1  10118  isf32lem2  10119  isf34lem4  10142  hsmexlem4  10194  axcc3  10203  domtriomlem  10207  axdc3lem2  10216  axdc4lem  10220  axcclem  10222  axdclem  10284  alephval2  10337  winainflem  10458  eltskm  10608  squeeze0  11887  lbreu  11934  nnsub  12026  ublbneg  12682  zmax  12694  zbtwnre  12695  xrub  13055  infmremnf  13086  infmrp1  13087  fzrevral  13350  axdc4uzlem  13712  faclbnd4lem4  14019  ccatalpha  14307  wrdind  14444  wrd2ind  14445  reuccatpfxs1lem  14468  recan  15057  cau3lem  15075  caubnd2  15078  climrlim2  15265  climshftlem  15292  rlimcld2  15296  subcn2  15313  isercoll  15388  climcau  15391  serf0  15401  iseralt  15405  isumrpcl  15564  clim2prod  15609  ntrivcvgfvn0  15620  sqrt2irr  15967  ndvdssub  16127  dfgcd2  16263  lcmf  16347  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  lcmfunsnlem2lem2  16353  lcmfdvdsb  16357  coprmgcdb  16363  coprmdvds1  16366  coprmprod  16375  coprmproddvdslem  16376  nprm  16402  dvdsprm  16417  coprm  16425  pcmpt  16602  pcmptdvds  16604  pcfac  16609  prmpwdvds  16614  unbenlem  16618  vdwlem10  16700  vdwlem13  16703  vdwnnlem1  16705  prmdvdsprmop  16753  prmgaplem7  16767  catideu  17393  initoid  17725  termoid  17726  initoeu1  17735  termoeu1  17742  isdrs2  18033  lublecllem  18087  lubun  18242  lidrididd  18363  sgrp2rid2ex  18575  dfgrp2  18613  grpidinv2  18643  dfgrp3lem  18682  issubg4  18783  efgi  19334  efgi2  19340  dprdss  19641  srgrz  19771  srglz  19772  srgisid  19773  f1rhm0to0ALT  19994  islmodd  20138  rmodislmod  20200  rmodislmodOLD  20201  islmhm2  20309  rrgeq0i  20569  ip2eq  20867  mvrf1  21203  cply1mul  21474  isclo2  22248  cnpnei  22424  cncls  22434  lmss  22458  cnt0  22506  isnrm2  22518  isreg2  22537  tgcmp  22561  uncmp  22563  dfconn2  22579  1stcclb  22604  2ndcctbss  22615  comppfsc  22692  kgencn2  22717  ptpjpre1  22731  txlm  22808  kqfvima  22890  kqt0lem  22896  isr0  22897  nrmr0reg  22909  fgss2  23034  isufil2  23068  cfinufil  23088  flimopn  23135  fbflim2  23137  flfneii  23152  cnpflf  23161  fclssscls  23178  fclsnei  23179  fclsrest  23184  flimfnfcls  23188  fclscmp  23190  isfcf  23194  fcfnei  23195  alexsubALTlem3  23209  alexsubALTlem4  23210  alexsubALT  23211  tsmsgsum  23299  tsmsres  23304  tsmsxplem1  23313  ustincl  23368  ustdiag  23369  ustinvel  23370  ustexhalf  23371  cfiluexsm  23451  psmet0  23470  prdsbl  23656  metss  23673  metcnp3  23705  isngp4  23777  nmoi  23901  mulc1cncf  24077  cncfco  24079  lebnumii  24138  iscfil3  24446  iscau2  24450  iscau4  24452  equivcfil  24472  equivcau  24473  lmcau  24486  ismbf  24801  ellimc3  25052  lhop1  25187  dvfsumlem4  25202  dvfsum2  25207  dgrco  25445  fta1  25477  aalioulem2  25502  aalioulem4  25504  ulmclm  25555  ulmshftlem  25557  ulmcaulem  25562  ulmcau  25563  ulmcn  25567  cxploglim  26136  ftalem3  26233  chtub  26369  dchrelbasd  26396  2sqlem6  26580  2sqlem10  26585  dchrisumlema  26645  dchrisumlem2  26647  dchrisumlem3  26648  dchrvmasumlem2  26655  pntpbnd1  26743  pntibnd  26750  pntleml  26768  brbtwn2  27282  colinearalg  27287  axcontlem4  27344  usgruspgrb  27560  cusgredg  27800  cusgrres  27824  usgredgsscusgredg  27835  fusgrn0degnn0  27875  wlk1walk  28015  wlkres  28047  wlkp1lem6  28055  wlkdlem2  28060  upgrwlkdvdelem  28113  pthdlem2lem  28144  lfgrn1cycl  28179  wwlksnredwwlkn  28269  wwlksnextproplem2  28284  clwwlkccatlem  28362  clwlkclwwlkf1lem3  28379  clwwisshclwwslemlem  28386  clwwlkf1  28422  clwwlkext2edg  28429  3cyclfrgrrn1  28658  n4cyclfrgr  28664  frgrwopregasn  28689  frgrwopregbsn  28690  isgrpo  28868  blocnilem  29175  ip2eqi  29227  htthlem  29288  hial0  29473  hial02  29474  hial2eq  29477  ocorth  29662  h1de2i  29924  pjjsi  30071  lnopunilem1  30381  lnophmlem1  30387  nmcexi  30397  riesz4i  30434  mdi  30666  mdbr3  30668  mdbr4  30669  dmdi  30673  dmdbr3  30676  dmdbr4  30677  dmdi4  30678  mdslmd1i  30700  atss  30717  atom1d  30724  atmd  30770  sumdmdlem2  30790  cdj1i  30804  cdj3i  30812  fnpreimac  31017  nn0min  31143  archiabllem1a  31454  archiabllem2a  31457  archiabl  31461  isarchiofld  31525  crefi  31806  pcmplfin  31819  fmcncfil  31890  sigaclcu  32094  unelsiga  32111  sigapildsys  32139  ldgenpisys  32143  measvun  32186  carsgclctunlem2  32295  sibfima  32314  fnrelpredd  33070  pfxwlk  33094  derangenlem  33142  subfacp1lem6  33156  resconn  33217  cvmcov  33234  cvmliftlem3  33258  cvmliftphtlem  33288  satfdmfmla  33371  mclsax  33540  dfon2lem6  33773  poseq  33811  soseq  33812  naddelim  33847  nolt02o  33907  noresle  33909  nosupbnd1lem1  33920  nosupbnd1lem4  33923  nosupbnd2lem1  33927  nosupbnd2  33928  nocvxminlem  33981  madebdaylemold  34087  fwddifnp1  34476  opnrebl2  34519  nn0prpwlem  34520  nn0prpw  34521  neibastop2lem  34558  neibastop2  34559  filnetlem4  34579  bj-mooreset  35282  bj-ismoored0  35286  dfgcd3  35504  fin2so  35773  poimirlem25  35811  poimirlem29  35815  poimir  35819  mbfresfi  35832  ftc1cnnclem  35857  seqpo  35914  incsequz  35915  mettrifi  35924  geomcau  35926  caushft  35928  sstotbnd2  35941  equivtotbnd  35945  totbndbnd  35956  ismtybndlem  35973  heibor1lem  35976  bfplem2  35990  opidonOLD  36019  exidu1  36023  rngoideu  36070  isdrngo2  36125  unichnidl  36198  lsat0cv  37054  lcvexchlem4  37058  lcvexchlem5  37059  eqlkr3  37122  lub0N  37210  glb0N  37214  cvrnbtwn  37292  ltrneq2  38169  trlval2  38184  lpolsatN  39509  lpolpolsatN  39510  hdmap14lem12  39900  isdomn4  40179  fsuppind  40286  nna4b4nsq  40504  incssnn0  40540  lnmlssfg  40912  unxpwdom3  40927  neik0pk1imk0  41664  ismnushort  41926  fnchoice  42579  monoordxrv  43029  monoord2xrv  43031  limcrecl  43177  fourierdlem54  43708  fourierdlem103  43757  fourierdlem104  43758  euoreqb  44612  smonoord  44834  iccpartlt  44887  iccpartgt  44890  iccpartdisj  44900  paireqne  44974  fmtnodvds  45007  perfectALTVlem2  45185  sbgoldbwt  45240  sbgoldbst  45241  sgoldbeven3prm  45246  mogoldbb  45248  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  bgoldbnnsum3prm  45267  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbndlem4  45271  bgoldbtbnd  45272  tgblthelfgott  45278  tgoldbach  45280  isomuspgrlem2c  45293  isomuspgrlem2d  45294  lcosslsp  45790  linindslinci  45800  lindslinindsimp1  45809  ldepsnlinclem1  45857  ldepsnlinclem2  45858  iscnrm3r  46253