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

Theorem rspcv 3566
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2142, ax-11 2158, ax-12 2175. (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 485 . 2 ((𝐴𝐵𝑥 = 𝐴) → (𝜑𝜓))
41, 3rspcdv 3563 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2111  wral 3106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111
This theorem is referenced by:  rspccv  3568  rspcva  3569  rspccva  3570  rspcdva  3573  rspc2v  3581  rspc3v  3584  rr19.3v  3607  rr19.28v  3608  rspsbc  3808  rspc2vd  3877  intmin  4858  ralxfrALT  5281  somo  5474  fr2nr  5497  weniso  7086  fr3nr  7474  limuni3  7547  tfinds  7554  funcnvuni  7618  suppfnss  7838  onnseq  7964  smo11  7984  tfrlem9  8004  tz7.49  8064  omeulem1  8191  oeordi  8196  nneneq  8684  frfi  8747  unblem2  8755  unbnn2  8759  xpfi  8773  ordiso2  8963  cantnflem1  9136  rankunb  9263  tcrank  9297  carduni  9394  dfac8alem  9440  alephinit  9506  aceq3lem  9531  dfac5  9539  dfac12r  9557  dfac12k  9558  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  lbreu  11578  nnsub  11669  ublbneg  12321  zmax  12333  zbtwnre  12334  xrub  12693  infmremnf  12724  infmrp1  12725  fzrevral  12987  axdc4uzlem  13346  faclbnd4lem4  13652  ccatalpha  13938  wrdind  14075  wrd2ind  14076  reuccatpfxs1lem  14099  recan  14688  cau3lem  14706  caubnd2  14709  climrlim2  14896  climshftlem  14923  rlimcld2  14927  subcn2  14943  isercoll  15016  climcau  15019  serf0  15029  iseralt  15033  isumrpcl  15190  clim2prod  15236  ntrivcvgfvn0  15247  sqrt2irr  15594  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  16938  initoid  17257  termoid  17258  initoeu1  17263  termoeu1  17270  isdrs2  17541  lublecllem  17590  lubun  17725  lidrididd  17872  sgrp2rid2ex  18084  dfgrp2  18120  grpidinv2  18150  dfgrp3lem  18189  issubg4  18290  efgi  18837  efgi2  18843  dprdss  19144  srgrz  19269  srglz  19270  srgisid  19271  f1rhm0to0ALT  19489  islmodd  19633  rmodislmod  19695  islmhm2  19803  rrgeq0i  20055  ip2eq  20342  mvrf1  20663  cply1mul  20923  isclo2  21693  cnpnei  21869  cncls  21879  lmss  21903  cnt0  21951  isnrm2  21963  isreg2  21982  tgcmp  22006  uncmp  22008  dfconn2  22024  1stcclb  22049  2ndcctbss  22060  comppfsc  22137  kgencn2  22162  ptpjpre1  22176  txlm  22253  kqfvima  22335  kqt0lem  22341  isr0  22342  nrmr0reg  22354  fgss2  22479  isufil2  22513  cfinufil  22533  flimopn  22580  fbflim2  22582  flfneii  22597  cnpflf  22606  fclssscls  22623  fclsnei  22624  fclsrest  22629  flimfnfcls  22633  fclscmp  22635  isfcf  22639  fcfnei  22640  alexsubALTlem3  22654  alexsubALTlem4  22655  alexsubALT  22656  tsmsgsum  22744  tsmsres  22749  tsmsxplem1  22758  ustincl  22813  ustdiag  22814  ustinvel  22815  ustexhalf  22816  cfiluexsm  22896  psmet0  22915  prdsbl  23098  metss  23115  metcnp3  23147  isngp4  23218  nmoi  23334  mulc1cncf  23510  cncfco  23512  lebnumii  23571  iscfil3  23877  iscau2  23881  iscau4  23883  equivcfil  23903  equivcau  23904  lmcau  23917  ismbf  24232  ellimc3  24482  lhop1  24617  dvfsumlem4  24632  dvfsum2  24637  dgrco  24872  fta1  24904  aalioulem2  24929  aalioulem4  24931  ulmclm  24982  ulmshftlem  24984  ulmcaulem  24989  ulmcau  24990  ulmcn  24994  cxploglim  25563  ftalem3  25660  chtub  25796  dchrelbasd  25823  2sqlem6  26007  2sqlem10  26012  dchrisumlema  26072  dchrisumlem2  26074  dchrisumlem3  26075  dchrvmasumlem2  26082  pntpbnd1  26170  pntibnd  26177  pntleml  26195  brbtwn2  26699  colinearalg  26704  axcontlem4  26761  usgruspgrb  26974  cusgredg  27214  cusgrres  27238  usgredgsscusgredg  27249  fusgrn0degnn0  27289  wlk1walk  27428  wlkres  27460  wlkp1lem6  27468  wlkdlem2  27473  upgrwlkdvdelem  27525  pthdlem2lem  27556  lfgrn1cycl  27591  wwlksnredwwlkn  27681  wwlksnextproplem2  27696  clwwlkccatlem  27774  clwlkclwwlkf1lem3  27791  clwwisshclwwslemlem  27798  clwwlkf1  27834  clwwlkext2edg  27841  3cyclfrgrrn1  28070  n4cyclfrgr  28076  frgrwopregasn  28101  frgrwopregbsn  28102  isgrpo  28280  blocnilem  28587  ip2eqi  28639  htthlem  28700  hial0  28885  hial02  28886  hial2eq  28889  ocorth  29074  h1de2i  29336  pjjsi  29483  lnopunilem1  29793  lnophmlem1  29799  nmcexi  29809  riesz4i  29846  mdi  30078  mdbr3  30080  mdbr4  30081  dmdi  30085  dmdbr3  30088  dmdbr4  30089  dmdi4  30090  mdslmd1i  30112  atss  30129  atom1d  30136  atmd  30182  sumdmdlem2  30202  cdj1i  30216  cdj3i  30224  fnpreimac  30434  nn0min  30562  archiabllem1a  30870  archiabllem2a  30873  archiabl  30877  isarchiofld  30941  crefi  31200  pcmplfin  31213  fmcncfil  31284  sigaclcu  31486  unelsiga  31503  sigapildsys  31531  ldgenpisys  31535  measvun  31578  carsgclctunlem2  31687  sibfima  31706  pfxwlk  32480  derangenlem  32528  subfacp1lem5  32541  subfacp1lem6  32542  resconn  32603  cvmcov  32620  cvmliftlem3  32644  cvmliftphtlem  32674  satfdmfmla  32757  mclsax  32926  dfon2lem6  33143  poseq  33205  soseq  33206  nolt02o  33309  noresle  33310  noprefixmo  33312  nosupbnd1lem1  33318  nosupbnd1lem4  33321  nosupbnd2lem1  33325  nosupbnd2  33326  nocvxminlem  33357  fwddifnp1  33736  opnrebl2  33779  nn0prpwlem  33780  nn0prpw  33781  neibastop2lem  33818  neibastop2  33819  filnetlem4  33839  bj-mooreset  34514  bj-ismoored0  34518  dfgcd3  34735  fin2so  35041  poimirlem25  35079  poimirlem29  35083  poimir  35087  mbfresfi  35100  ftc1cnnclem  35125  seqpo  35182  incsequz  35183  mettrifi  35192  geomcau  35194  caushft  35196  sstotbnd2  35209  equivtotbnd  35213  totbndbnd  35224  ismtybndlem  35241  heibor1lem  35244  bfplem2  35258  opidonOLD  35287  exidu1  35291  rngoideu  35338  isdrngo2  35393  unichnidl  35466  lsat0cv  36326  lcvexchlem4  36330  lcvexchlem5  36331  eqlkr3  36394  lub0N  36482  glb0N  36486  cvrnbtwn  36564  ltrneq2  37441  trlval2  37456  lpolsatN  38781  lpolpolsatN  38782  hdmap14lem12  39172  fsuppind  39451  incssnn0  39647  lnmlssfg  40019  unxpwdom3  40034  neik0pk1imk0  40745  fnchoice  41653  monoordxrv  42116  monoord2xrv  42118  limcrecl  42266  fourierdlem54  42797  fourierdlem103  42846  fourierdlem104  42847  euoreqb  43660  smonoord  43883  iccpartlt  43936  iccpartgt  43939  iccpartdisj  43949  paireqne  44023  fmtnodvds  44056  perfectALTVlem2  44235  sbgoldbwt  44290  sbgoldbst  44291  sgoldbeven3prm  44296  mogoldbb  44298  nnsum4primesodd  44309  nnsum4primesoddALTV  44310  bgoldbnnsum3prm  44317  bgoldbtbndlem2  44319  bgoldbtbndlem3  44320  bgoldbtbndlem4  44321  bgoldbtbnd  44322  tgblthelfgott  44328  tgoldbach  44330  isomuspgrlem2c  44343  isomuspgrlem2d  44344  lcosslsp  44842  linindslinci  44852  lindslinindsimp1  44861  ldepsnlinclem1  44909  ldepsnlinclem2  44910
  Copyright terms: Public domain W3C validator