Theorem rspcv 3547

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068

This theorem is referenced by:  rspccv  3549  rspcva  3550  rspccva  3551  rspcdva  3554  rspc2v  3562  rspc3v  3565  rr19.3v  3591  rr19.28v  3592  rspsbc  3808  rspc2vd  3879  intmin  4896  ralxfrALT  5333  somo  5531  fr2nr  5558  weniso  7205  fr3nr  7600  limuni3  7674  tfinds  7681  funcnvuni  7752  suppfnss  7976  onnseq  8146  smo11  8166  tfrlem9  8187  tz7.49  8246  omeulem1  8375  oeordi  8380  nneneq  8896  frfi  8989  unblem2  8997  unbnn2  9001  xpfi  9015  ordiso2  9204  cantnflem1  9377  frins3  9444  rankunb  9539  tcrank  9573  carduni  9670  dfac8alem  9716  alephinit  9782  aceq3lem  9807  dfac5  9815  dfac12r  9833  dfac12k  9834  pwsdompw  9891  cflm  9937  isf32lem1  10040  isf32lem2  10041  isf34lem4  10064  hsmexlem4  10116  axcc3  10125  domtriomlem  10129  axdc3lem2  10138  axdc4lem  10142  axcclem  10144  axdclem  10206  alephval2  10259  winainflem  10380  eltskm  10530  squeeze0  11808  lbreu  11855  nnsub  11947  ublbneg  12602  zmax  12614  zbtwnre  12615  xrub  12975  infmremnf  13006  infmrp1  13007  fzrevral  13270  axdc4uzlem  13631  faclbnd4lem4  13938  ccatalpha  14226  wrdind  14363  wrd2ind  14364  reuccatpfxs1lem  14387  recan  14976  cau3lem  14994  caubnd2  14997  climrlim2  15184  climshftlem  15211  rlimcld2  15215  subcn2  15232  isercoll  15307  climcau  15310  serf0  15320  iseralt  15324  isumrpcl  15483  clim2prod  15528  ntrivcvgfvn0  15539  sqrt2irr  15886  ndvdssub  16046  dfgcd2  16182  lcmf  16266  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  lcmfdvdsb  16276  coprmgcdb  16282  coprmdvds1  16285  coprmprod  16294  coprmproddvdslem  16295  nprm  16321  dvdsprm  16336  coprm  16344  pcmpt  16521  pcmptdvds  16523  pcfac  16528  prmpwdvds  16533  unbenlem  16537  vdwlem10  16619  vdwlem13  16622  vdwnnlem1  16624  prmdvdsprmop  16672  prmgaplem7  16686  catideu  17301  initoid  17632  termoid  17633  initoeu1  17642  termoeu1  17649  isdrs2  17939  lublecllem  17993  lubun  18148  lidrididd  18269  sgrp2rid2ex  18481  dfgrp2  18519  grpidinv2  18549  dfgrp3lem  18588  issubg4  18689  efgi  19240  efgi2  19246  dprdss  19547  srgrz  19677  srglz  19678  srgisid  19679  f1rhm0to0ALT  19900  islmodd  20044  rmodislmod  20106  rmodislmodOLD  20107  islmhm2  20215  rrgeq0i  20473  ip2eq  20770  mvrf1  21104  cply1mul  21375  isclo2  22147  cnpnei  22323  cncls  22333  lmss  22357  cnt0  22405  isnrm2  22417  isreg2  22436  tgcmp  22460  uncmp  22462  dfconn2  22478  1stcclb  22503  2ndcctbss  22514  comppfsc  22591  kgencn2  22616  ptpjpre1  22630  txlm  22707  kqfvima  22789  kqt0lem  22795  isr0  22796  nrmr0reg  22808  fgss2  22933  isufil2  22967  cfinufil  22987  flimopn  23034  fbflim2  23036  flfneii  23051  cnpflf  23060  fclssscls  23077  fclsnei  23078  fclsrest  23083  flimfnfcls  23087  fclscmp  23089  isfcf  23093  fcfnei  23094  alexsubALTlem3  23108  alexsubALTlem4  23109  alexsubALT  23110  tsmsgsum  23198  tsmsres  23203  tsmsxplem1  23212  ustincl  23267  ustdiag  23268  ustinvel  23269  ustexhalf  23270  cfiluexsm  23350  psmet0  23369  prdsbl  23553  metss  23570  metcnp3  23602  isngp4  23674  nmoi  23798  mulc1cncf  23974  cncfco  23976  lebnumii  24035  iscfil3  24342  iscau2  24346  iscau4  24348  equivcfil  24368  equivcau  24369  lmcau  24382  ismbf  24697  ellimc3  24948  lhop1  25083  dvfsumlem4  25098  dvfsum2  25103  dgrco  25341  fta1  25373  aalioulem2  25398  aalioulem4  25400  ulmclm  25451  ulmshftlem  25453  ulmcaulem  25458  ulmcau  25459  ulmcn  25463  cxploglim  26032  ftalem3  26129  chtub  26265  dchrelbasd  26292  2sqlem6  26476  2sqlem10  26481  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  dchrvmasumlem2  26551  pntpbnd1  26639  pntibnd  26646  pntleml  26664  brbtwn2  27176  colinearalg  27181  axcontlem4  27238  usgruspgrb  27454  cusgredg  27694  cusgrres  27718  usgredgsscusgredg  27729  fusgrn0degnn0  27769  wlk1walk  27908  wlkres  27940  wlkp1lem6  27948  wlkdlem2  27953  upgrwlkdvdelem  28005  pthdlem2lem  28036  lfgrn1cycl  28071  wwlksnredwwlkn  28161  wwlksnextproplem2  28176  clwwlkccatlem  28254  clwlkclwwlkf1lem3  28271  clwwisshclwwslemlem  28278  clwwlkf1  28314  clwwlkext2edg  28321  3cyclfrgrrn1  28550  n4cyclfrgr  28556  frgrwopregasn  28581  frgrwopregbsn  28582  isgrpo  28760  blocnilem  29067  ip2eqi  29119  htthlem  29180  hial0  29365  hial02  29366  hial2eq  29369  ocorth  29554  h1de2i  29816  pjjsi  29963  lnopunilem1  30273  lnophmlem1  30279  nmcexi  30289  riesz4i  30326  mdi  30558  mdbr3  30560  mdbr4  30561  dmdi  30565  dmdbr3  30568  dmdbr4  30569  dmdi4  30570  mdslmd1i  30592  atss  30609  atom1d  30616  atmd  30662  sumdmdlem2  30682  cdj1i  30696  cdj3i  30704  fnpreimac  30910  nn0min  31036  archiabllem1a  31347  archiabllem2a  31350  archiabl  31354  isarchiofld  31418  crefi  31699  pcmplfin  31712  fmcncfil  31783  sigaclcu  31985  unelsiga  32002  sigapildsys  32030  ldgenpisys  32034  measvun  32077  carsgclctunlem2  32186  sibfima  32205  fnrelpredd  32961  pfxwlk  32985  derangenlem  33033  subfacp1lem6  33047  resconn  33108  cvmcov  33125  cvmliftlem3  33149  cvmliftphtlem  33179  satfdmfmla  33262  mclsax  33431  dfon2lem6  33670  ttrcltr  33702  ttrclss  33706  ttrclselem2  33712  poseq  33729  soseq  33730  naddelim  33765  nolt02o  33825  noresle  33827  nosupbnd1lem1  33838  nosupbnd1lem4  33841  nosupbnd2lem1  33845  nosupbnd2  33846  nocvxminlem  33899  madebdaylemold  34005  fwddifnp1  34394  opnrebl2  34437  nn0prpwlem  34438  nn0prpw  34439  neibastop2lem  34476  neibastop2  34477  filnetlem4  34497  bj-mooreset  35200  bj-ismoored0  35204  dfgcd3  35422  fin2so  35691  poimirlem25  35729  poimirlem29  35733  poimir  35737  mbfresfi  35750  ftc1cnnclem  35775  seqpo  35832  incsequz  35833  mettrifi  35842  geomcau  35844  caushft  35846  sstotbnd2  35859  equivtotbnd  35863  totbndbnd  35874  ismtybndlem  35891  heibor1lem  35894  bfplem2  35908  opidonOLD  35937  exidu1  35941  rngoideu  35988  isdrngo2  36043  unichnidl  36116  lsat0cv  36974  lcvexchlem4  36978  lcvexchlem5  36979  eqlkr3  37042  lub0N  37130  glb0N  37134  cvrnbtwn  37212  ltrneq2  38089  trlval2  38104  lpolsatN  39429  lpolpolsatN  39430  hdmap14lem12  39820  isdomn4  40100  fsuppind  40202  nna4b4nsq  40413  incssnn0  40449  lnmlssfg  40821  unxpwdom3  40836  neik0pk1imk0  41546  ismnushort  41808  fnchoice  42461  monoordxrv  42912  monoord2xrv  42914  limcrecl  43060  fourierdlem54  43591  fourierdlem103  43640  fourierdlem104  43641  euoreqb  44488  smonoord  44711  iccpartlt  44764  iccpartgt  44767  iccpartdisj  44777  paireqne  44851  fmtnodvds  44884  perfectALTVlem2  45062  sbgoldbwt  45117  sbgoldbst  45118  sgoldbeven3prm  45123  mogoldbb  45125  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  bgoldbnnsum3prm  45144  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbndlem4  45148  bgoldbtbnd  45149  tgblthelfgott  45155  tgoldbach  45157  isomuspgrlem2c  45170  isomuspgrlem2d  45171  lcosslsp  45667  linindslinci  45677  lindslinindsimp1  45686  ldepsnlinclem1  45734  ldepsnlinclem2  45735  iscnrm3r  46130