Theorem rspcv 3556

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054

This theorem is referenced by:  rspccv  3557  rspcva  3558  rspccva  3559  rspcdva  3561  rspc2v  3571  rspc3v  3576  rspc4v  3580  rr19.3v  3605  rr19.28v  3606  rspsbc  3811  rspc2vd  3879  intmin  4898  ralxfrALT  5344  somo  5565  fr2nr  5595  weniso  7298  fr3nr  7715  limuni3  7792  tfinds  7800  funcnvuni  7872  resf1extb  7874  poseq  8098  soseq  8099  suppfnss  8129  onnseq  8274  smo11  8294  tfrlem9  8314  tz7.49  8374  omeulem1  8507  oeordi  8513  naddelim  8612  nneneq  9130  frfi  9185  unblem2  9193  unbnn2  9197  ordiso2  9420  cantnflem1  9601  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  frins3  9670  rankunb  9765  tcrank  9799  carduni  9896  dfac8alem  9942  alephinit  10008  aceq3lem  10033  dfac5  10042  dfac12r  10060  dfac12k  10061  pwsdompw  10116  cflm  10163  isf32lem1  10266  isf32lem2  10267  isf34lem4  10290  hsmexlem4  10342  axcc3  10351  domtriomlem  10355  axdc3lem2  10364  axdc4lem  10368  axcclem  10370  axdclem  10432  alephval2  10486  winainflem  10607  eltskm  10757  squeeze0  12050  lbreu  12097  nnsub  12212  ublbneg  12874  zmax  12886  zbtwnre  12887  xrub  13255  infmremnf  13287  infmrp1  13288  fzrevral  13557  axdc4uzlem  13936  faclbnd4lem4  14249  ccatalpha  14547  wrdind  14675  wrd2ind  14676  reuccatpfxs1lem  14699  recan  15290  cau3lem  15308  caubnd2  15311  climrlim2  15500  climshftlem  15527  rlimcld2  15531  subcn2  15548  isercoll  15621  climcau  15624  serf0  15634  iseralt  15638  isumrpcl  15799  clim2prod  15844  ntrivcvgfvn0  15855  sqrt2irr  16207  ndvdssub  16369  dfgcd2  16506  lcmf  16593  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfdvdsb  16603  coprmgcdb  16609  coprmdvds1  16612  coprmprod  16621  coprmproddvdslem  16622  nprm  16648  dvdsprm  16664  coprm  16672  pcmpt  16854  pcmptdvds  16856  pcfac  16861  prmpwdvds  16866  unbenlem  16870  vdwlem10  16952  vdwlem13  16955  vdwnnlem1  16957  prmdvdsprmop  17005  prmgaplem7  17019  catideu  17632  initoid  17959  termoid  17960  initoeu1  17969  termoeu1  17976  isdrs2  18263  lublecllem  18315  lubun  18472  lidrididd  18629  sgrp2rid2ex  18889  dfgrp2  18929  grpidinv2  18964  dfgrp3lem  19005  issubg4  19112  efgi  19685  efgi2  19691  dprdss  19997  srgrz  20179  srglz  20180  srgisid  20181  rrgeq0i  20671  isdomn4  20688  islmodd  20856  rmodislmod  20920  islmhm2  21028  rnglidlmcl  21209  ip2eq  21628  mvrf1  21960  psdmul  22154  cply1mul  22282  isclo2  23071  cnpnei  23247  cncls  23257  lmss  23281  cnt0  23329  isnrm2  23341  isreg2  23360  tgcmp  23384  uncmp  23386  dfconn2  23402  1stcclb  23427  2ndcctbss  23438  comppfsc  23515  kgencn2  23540  ptpjpre1  23554  txlm  23631  kqfvima  23713  kqt0lem  23719  isr0  23720  nrmr0reg  23732  fgss2  23857  isufil2  23891  cfinufil  23911  flimopn  23958  fbflim2  23960  flfneii  23975  cnpflf  23984  fclssscls  24001  fclsnei  24002  fclsrest  24007  flimfnfcls  24011  fclscmp  24013  isfcf  24017  fcfnei  24018  alexsubALTlem3  24032  alexsubALTlem4  24033  alexsubALT  24034  tsmsgsum  24122  tsmsres  24127  tsmsxplem1  24136  ustincl  24191  ustdiag  24192  ustinvel  24193  ustexhalf  24194  cfiluexsm  24272  psmet0  24291  prdsbl  24474  metss  24491  metcnp3  24523  isngp4  24595  nmoi  24711  mulc1cncf  24890  cncfco  24892  lebnumii  24951  iscfil3  25258  iscau2  25262  iscau4  25264  equivcfil  25284  equivcau  25285  lmcau  25298  ismbf  25613  ellimc3  25864  lhop1  25999  dvfsumlem4  26014  dvfsum2  26019  dgrco  26258  fta1  26292  aalioulem2  26317  aalioulem4  26319  ulmclm  26370  ulmshftlem  26372  ulmcaulem  26377  ulmcau  26378  ulmcn  26382  cxploglim  26959  ftalem3  27056  chtub  27193  dchrelbasd  27220  2sqlem6  27404  2sqlem10  27409  dchrisumlema  27469  dchrisumlem2  27471  dchrisumlem3  27472  dchrvmasumlem2  27479  pntpbnd1  27567  pntibnd  27574  pntleml  27592  nolt02o  27677  noresle  27679  nosupbnd1lem1  27690  nosupbnd1lem4  27693  nosupbnd2lem1  27697  nosupbnd2  27698  nocvxminlem  27764  madebdaylemold  27908  n0subs  28373  z12zsodd  28492  brbtwn2  28992  colinearalg  28997  axcontlem4  29054  usgruspgrb  29270  cusgredg  29511  cusgrres  29535  usgredgsscusgredg  29546  fusgrn0degnn0  29586  wlk1walk  29725  wlkres  29755  wlkp1lem6  29763  wlkdlem2  29768  upgrwlkdvdelem  29822  pthdlem2lem  29853  lfgrn1cycl  29891  wwlksnredwwlkn  29981  wwlksnextproplem2  29996  clwwlkccatlem  30077  clwlkclwwlkf1lem3  30094  clwwisshclwwslemlem  30101  clwwlkf1  30137  clwwlkext2edg  30144  3cyclfrgrrn1  30373  n4cyclfrgr  30379  frgrwopregasn  30404  frgrwopregbsn  30405  isgrpo  30586  blocnilem  30893  ip2eqi  30945  htthlem  31006  hial0  31191  hial02  31192  hial2eq  31195  ocorth  31380  h1de2i  31642  pjjsi  31789  lnopunilem1  32099  lnophmlem1  32105  nmcexi  32115  riesz4i  32152  mdi  32384  mdbr3  32386  mdbr4  32387  dmdi  32391  dmdbr3  32394  dmdbr4  32395  dmdi4  32396  mdslmd1i  32418  atss  32435  atom1d  32442  atmd  32488  sumdmdlem2  32508  cdj1i  32522  cdj3i  32530  fnpreimac  32762  nn0min  32913  archiabllem1a  33272  archiabllem2a  33275  archiabl  33279  isarchiofld  33280  trisecnconstr  33976  crefi  34031  pcmplfin  34044  fmcncfil  34115  sigaclcu  34301  unelsiga  34318  sigapildsys  34346  ldgenpisys  34350  measvun  34393  carsgclctunlem2  34503  sibfima  34522  fnrelpredd  35272  fineqvnttrclse  35305  fineqvinfep  35306  pfxwlk  35352  derangenlem  35399  subfacp1lem6  35413  resconn  35474  cvmcov  35491  cvmliftlem3  35515  cvmliftphtlem  35545  satfdmfmla  35628  mclsax  35797  dfon2lem6  36014  fwddifnp1  36393  opnrebl2  36549  nn0prpwlem  36550  nn0prpw  36551  neibastop2lem  36588  neibastop2  36589  filnetlem4  36609  dfttc4  36758  bj-mooreset  37460  bj-ismoored0  37464  dfgcd3  37684  fin2so  37974  poimirlem25  38012  poimirlem29  38016  poimir  38020  mbfresfi  38033  ftc1cnnclem  38058  seqpo  38114  incsequz  38115  mettrifi  38124  geomcau  38126  caushft  38128  sstotbnd2  38141  equivtotbnd  38145  totbndbnd  38156  ismtybndlem  38173  heibor1lem  38176  bfplem2  38190  opidonOLD  38219  exidu1  38223  rngoideu  38270  isdrngo2  38325  unichnidl  38398  lsat0cv  39525  lcvexchlem4  39529  lcvexchlem5  39530  eqlkr3  39593  lub0N  39681  glb0N  39685  cvrnbtwn  39763  ltrneq2  40640  trlval2  40655  lpolsatN  41980  lpolpolsatN  41981  hdmap14lem12  42371  fsuppind  43040  nna4b4nsq  43110  incssnn0  43160  lnmlssfg  43525  unxpwdom3  43540  neik0pk1imk0  44491  ismnushort  44745  fnchoice  45477  monoordxrv  45924  monoord2xrv  45926  limcrecl  46074  fourierdlem54  46603  fourierdlem103  46652  fourierdlem104  46653  euoreqb  47572  smonoord  47840  iccpartlt  47899  iccpartgt  47902  iccpartdisj  47912  paireqne  47986  fmtnodvds  48022  perfectALTVlem2  48213  sbgoldbwt  48268  sbgoldbst  48269  sgoldbeven3prm  48274  mogoldbb  48276  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  bgoldbnnsum3prm  48295  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbndlem4  48299  bgoldbtbnd  48300  tgblthelfgott  48306  tgoldbach  48308  grimuhgr  48378  grimcnv  48379  grimco  48380  uhgrimedgi  48381  isuspgrim0  48385  upgrimwlklem5  48392  uhgrimisgrgriclem  48421  clnbgrgrimlem  48424  clnbgrgrim  48425  grimedg  48426  uspgrlimlem3  48481  uspgrlimlem4  48482  grlimedgclnbgr  48486  grlimgrtrilem2  48493  grlimgrtri  48494  grilcbri2  48502  grlicsym  48504  grlictr  48506  clnbgr3stgrgrlim  48510  clnbgr3stgrgrlic  48511  lcosslsp  48929  linindslinci  48939  lindslinindsimp1  48948  ldepsnlinclem1  48996  ldepsnlinclem2  48997  iscnrm3r  49438  initc  49581  termc2  50008