MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspcv Structured version   Visualization version   GIF version

Theorem rspcv 3617
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2136, ax-11 2151, ax-12 2167. (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
StepHypRef Expression
1 id 22 . 2 (𝐴𝐵𝐴𝐵)
2 rspcv.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32adantl 482 . 2 ((𝐴𝐵𝑥 = 𝐴) → (𝜑𝜓))
41, 3rspcdv 3614 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  wral 3138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893  df-ral 3143
This theorem is referenced by:  rspccv  3619  rspcva  3620  rspccva  3621  rspcdva  3624  rspc2v  3632  rspc3v  3635  rr19.3v  3660  rr19.28v  3661  rspsbc  3861  rspc2vd  3931  intmin  4889  ralxfrALT  5307  somo  5504  fr2nr  5527  weniso  7096  fr3nr  7482  limuni3  7555  tfinds  7562  funcnvuni  7624  suppfnss  7846  onnseq  7972  smo11  7992  tfrlem9  8012  tz7.49  8072  omeulem1  8198  oeordi  8203  nneneq  8689  frfi  8752  unblem2  8760  unbnn2  8764  xpfi  8778  ordiso2  8968  cantnflem1  9141  rankunb  9268  tcrank  9302  carduni  9399  dfac8alem  9444  alephinit  9510  aceq3lem  9535  dfac5  9543  dfac12r  9561  dfac12k  9562  pwsdompw  9615  cflm  9661  isf32lem1  9764  isf32lem2  9765  isf34lem4  9788  hsmexlem4  9840  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc4lem  9866  axcclem  9868  axdclem  9930  alephval2  9983  winainflem  10104  eltskm  10254  squeeze0  11532  fiminreOLD  11579  lbreu  11580  nnsub  11670  ublbneg  12322  zmax  12334  zbtwnre  12335  xrub  12695  infmremnf  12726  infmrp1  12727  fzrevral  12982  axdc4uzlem  13341  faclbnd4lem4  13646  ccatalpha  13937  wrdind  14074  wrd2ind  14075  reuccatpfxs1lem  14098  recan  14686  cau3lem  14704  caubnd2  14707  climrlim2  14894  climshftlem  14921  rlimcld2  14925  subcn2  14941  isercoll  15014  climcau  15017  serf0  15027  iseralt  15031  isumrpcl  15188  clim2prod  15234  ntrivcvgfvn0  15245  sqrt2irr  15592  ndvdssub  15750  dfgcd2  15884  lcmf  15967  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  lcmfdvdsb  15977  coprmgcdb  15983  coprmdvds1  15986  coprmprod  15995  coprmproddvdslem  15996  nprm  16022  dvdsprm  16037  coprm  16045  pcmpt  16218  pcmptdvds  16220  pcfac  16225  prmpwdvds  16230  unbenlem  16234  vdwlem10  16316  vdwlem13  16319  vdwnnlem1  16321  prmdvdsprmop  16369  prmgaplem7  16383  catideu  16936  initoid  17255  termoid  17256  initoeu1  17261  termoeu1  17268  isdrs2  17539  lublecllem  17588  lubun  17723  lidrididd  17870  sgrp2rid2ex  18032  dfgrp2  18068  grpidinv2  18098  dfgrp3lem  18137  issubg4  18238  efgi  18776  efgi2  18782  dprdss  19082  srgrz  19207  srglz  19208  srgisid  19209  f1rhm0to0ALT  19425  islmodd  19571  rmodislmod  19633  islmhm2  19741  rrgeq0i  19992  mvrf1  20135  cply1mul  20392  ip2eq  20727  isclo2  21626  cnpnei  21802  cncls  21812  lmss  21836  cnt0  21884  isnrm2  21896  isreg2  21915  tgcmp  21939  uncmp  21941  dfconn2  21957  1stcclb  21982  2ndcctbss  21993  comppfsc  22070  kgencn2  22095  ptpjpre1  22109  txlm  22186  kqfvima  22268  kqt0lem  22274  isr0  22275  nrmr0reg  22287  fgss2  22412  isufil2  22446  cfinufil  22466  flimopn  22513  fbflim2  22515  flfneii  22530  cnpflf  22539  fclssscls  22556  fclsnei  22557  fclsrest  22562  flimfnfcls  22566  fclscmp  22568  isfcf  22572  fcfnei  22573  alexsubALTlem3  22587  alexsubALTlem4  22588  alexsubALT  22589  tsmsgsum  22676  tsmsres  22681  tsmsxplem1  22690  ustincl  22745  ustdiag  22746  ustinvel  22747  ustexhalf  22748  cfiluexsm  22828  psmet0  22847  prdsbl  23030  metss  23047  metcnp3  23079  isngp4  23150  nmoi  23266  mulc1cncf  23442  cncfco  23444  lebnumii  23499  iscfil3  23805  iscau2  23809  iscau4  23811  equivcfil  23831  equivcau  23832  lmcau  23845  ismbf  24158  ellimc3  24406  lhop1  24540  dvfsumlem4  24555  dvfsum2  24560  dgrco  24794  fta1  24826  aalioulem2  24851  aalioulem4  24853  ulmclm  24904  ulmshftlem  24906  ulmcaulem  24911  ulmcau  24912  ulmcn  24916  cxploglim  25483  ftalem3  25580  chtub  25716  dchrelbasd  25743  2sqlem6  25927  2sqlem10  25932  dchrisumlema  25992  dchrisumlem2  25994  dchrisumlem3  25995  dchrvmasumlem2  26002  pntpbnd1  26090  pntibnd  26097  pntleml  26115  brbtwn2  26619  colinearalg  26624  axcontlem4  26681  usgruspgrb  26894  cusgredg  27134  cusgrres  27158  usgredgsscusgredg  27169  fusgrn0degnn0  27209  wlk1walk  27348  wlkres  27380  wlkp1lem6  27388  wlkdlem2  27393  upgrwlkdvdelem  27445  pthdlem2lem  27476  lfgrn1cycl  27511  wwlksnredwwlkn  27601  wwlksnextproplem2  27617  clwwlkccatlem  27695  clwlkclwwlkf1lem3  27712  clwwisshclwwslemlem  27719  clwwlkf1  27756  clwwlkext2edg  27763  3cyclfrgrrn1  27992  n4cyclfrgr  27998  frgrwopregasn  28023  frgrwopregbsn  28024  isgrpo  28202  blocnilem  28509  ip2eqi  28561  htthlem  28622  hial0  28807  hial02  28808  hial2eq  28811  ocorth  28996  h1de2i  29258  pjjsi  29405  lnopunilem1  29715  lnophmlem1  29721  nmcexi  29731  riesz4i  29768  mdi  30000  mdbr3  30002  mdbr4  30003  dmdi  30007  dmdbr3  30010  dmdbr4  30011  dmdi4  30012  mdslmd1i  30034  atss  30051  atom1d  30058  atmd  30104  sumdmdlem2  30124  cdj1i  30138  cdj3i  30146  fnpreimac  30345  nn0min  30464  archiabllem1a  30748  archiabllem2a  30751  archiabl  30755  isarchiofld  30818  crefi  31011  pcmplfin  31024  fmcncfil  31074  sigaclcu  31276  unelsiga  31293  sigapildsys  31321  ldgenpisys  31325  measvun  31368  carsgclctunlem2  31477  sibfima  31496  pfxwlk  32268  derangenlem  32316  subfacp1lem5  32329  subfacp1lem6  32330  resconn  32391  cvmcov  32408  cvmliftlem3  32432  cvmliftphtlem  32462  satfdmfmla  32545  mclsax  32714  dfon2lem6  32931  poseq  32993  soseq  32994  nolt02o  33097  noresle  33098  noprefixmo  33100  nosupbnd1lem1  33106  nosupbnd1lem4  33109  nosupbnd2lem1  33113  nosupbnd2  33114  nocvxminlem  33145  fwddifnp1  33524  opnrebl2  33567  nn0prpwlem  33568  nn0prpw  33569  neibastop2lem  33606  neibastop2  33607  filnetlem4  33627  bj-mooreset  34289  bj-ismoored0  34293  dfgcd3  34488  fin2so  34761  poimirlem25  34799  poimirlem29  34803  poimir  34807  mbfresfi  34820  ftc1cnnclem  34847  seqpo  34905  incsequz  34906  mettrifi  34915  geomcau  34917  caushft  34919  sstotbnd2  34935  equivtotbnd  34939  totbndbnd  34950  ismtybndlem  34967  heibor1lem  34970  bfplem2  34984  opidonOLD  35013  exidu1  35017  rngoideu  35064  isdrngo2  35119  unichnidl  35192  lsat0cv  36051  lcvexchlem4  36055  lcvexchlem5  36056  eqlkr3  36119  lub0N  36207  glb0N  36211  cvrnbtwn  36289  ltrneq2  37166  trlval2  37181  lpolsatN  38506  lpolpolsatN  38507  hdmap14lem12  38897  incssnn0  39188  lnmlssfg  39560  unxpwdom3  39575  neik0pk1imk0  40277  fnchoice  41166  monoordxrv  41638  monoord2xrv  41640  limcrecl  41790  fourierdlem54  42326  fourierdlem103  42375  fourierdlem104  42376  euoreqb  43189  smonoord  43412  iccpartlt  43431  iccpartgt  43434  iccpartdisj  43444  paireqne  43520  fmtnodvds  43553  perfectALTVlem2  43734  sbgoldbwt  43789  sbgoldbst  43790  sgoldbeven3prm  43795  mogoldbb  43797  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  bgoldbnnsum3prm  43816  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  bgoldbtbndlem4  43820  bgoldbtbnd  43821  tgblthelfgott  43827  tgoldbach  43829  isomuspgrlem2c  43842  isomuspgrlem2d  43843  lcosslsp  44391  linindslinci  44401  lindslinindsimp1  44410  ldepsnlinclem1  44458  ldepsnlinclem2  44459
  Copyright terms: Public domain W3C validator