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

Theorem rspcv 3580
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
StepHypRef Expression
1 id 22 . 2 (𝐴𝐵𝐴𝐵)
2 rspcv.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32adantl 483 . 2 ((𝐴𝐵𝑥 = 𝐴) → (𝜑𝜓))
41, 3rspcdv 3576 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066
This theorem is referenced by:  rspccv  3581  rspcva  3582  rspccva  3583  rspcdva  3585  rspc2v  3593  rspc3v  3596  rspc4v  3598  rr19.3v  3624  rr19.28v  3625  rspsbc  3840  rspc2vd  3911  intmin  4934  ralxfrALT  5375  somo  5587  fr2nr  5616  weniso  7304  fr3nr  7711  limuni3  7793  tfinds  7801  funcnvuni  7873  poseq  8095  soseq  8096  suppfnss  8125  onnseq  8295  smo11  8315  tfrlem9  8336  tz7.49  8396  omeulem1  8534  oeordi  8539  naddelim  8637  nneneq  9160  nneneqOLD  9172  frfi  9239  unblem2  9247  unbnn2  9251  xpfiOLD  9269  ordiso2  9458  cantnflem1  9632  ttrcltr  9659  ttrclss  9663  ttrclselem2  9669  frins3  9698  rankunb  9793  tcrank  9827  carduni  9924  dfac8alem  9972  alephinit  10038  aceq3lem  10063  dfac5  10071  dfac12r  10089  dfac12k  10090  pwsdompw  10147  cflm  10193  isf32lem1  10296  isf32lem2  10297  isf34lem4  10320  hsmexlem4  10372  axcc3  10381  domtriomlem  10385  axdc3lem2  10394  axdc4lem  10398  axcclem  10400  axdclem  10462  alephval2  10515  winainflem  10636  eltskm  10786  squeeze0  12065  lbreu  12112  nnsub  12204  ublbneg  12865  zmax  12877  zbtwnre  12878  xrub  13238  infmremnf  13269  infmrp1  13270  fzrevral  13533  axdc4uzlem  13895  faclbnd4lem4  14203  ccatalpha  14488  wrdind  14617  wrd2ind  14618  reuccatpfxs1lem  14641  recan  15228  cau3lem  15246  caubnd2  15249  climrlim2  15436  climshftlem  15463  rlimcld2  15467  subcn2  15484  isercoll  15559  climcau  15562  serf0  15572  iseralt  15576  isumrpcl  15735  clim2prod  15780  ntrivcvgfvn0  15791  sqrt2irr  16138  ndvdssub  16298  dfgcd2  16434  lcmf  16516  lcmfunsnlem1  16520  lcmfunsnlem2lem1  16521  lcmfunsnlem2lem2  16522  lcmfdvdsb  16526  coprmgcdb  16532  coprmdvds1  16535  coprmprod  16544  coprmproddvdslem  16545  nprm  16571  dvdsprm  16586  coprm  16594  pcmpt  16771  pcmptdvds  16773  pcfac  16778  prmpwdvds  16783  unbenlem  16787  vdwlem10  16869  vdwlem13  16872  vdwnnlem1  16874  prmdvdsprmop  16922  prmgaplem7  16936  catideu  17562  initoid  17894  termoid  17895  initoeu1  17904  termoeu1  17911  isdrs2  18202  lublecllem  18256  lubun  18411  lidrididd  18532  sgrp2rid2ex  18744  dfgrp2  18782  grpidinv2  18813  dfgrp3lem  18852  issubg4  18954  efgi  19508  efgi2  19514  dprdss  19815  srgrz  19945  srglz  19946  srgisid  19947  f1rhm0to0ALT  20184  islmodd  20344  rmodislmod  20406  rmodislmodOLD  20407  islmhm2  20515  rrgeq0i  20775  ip2eq  21073  mvrf1  21410  cply1mul  21681  isclo2  22455  cnpnei  22631  cncls  22641  lmss  22665  cnt0  22713  isnrm2  22725  isreg2  22744  tgcmp  22768  uncmp  22770  dfconn2  22786  1stcclb  22811  2ndcctbss  22822  comppfsc  22899  kgencn2  22924  ptpjpre1  22938  txlm  23015  kqfvima  23097  kqt0lem  23103  isr0  23104  nrmr0reg  23116  fgss2  23241  isufil2  23275  cfinufil  23295  flimopn  23342  fbflim2  23344  flfneii  23359  cnpflf  23368  fclssscls  23385  fclsnei  23386  fclsrest  23391  flimfnfcls  23395  fclscmp  23397  isfcf  23401  fcfnei  23402  alexsubALTlem3  23416  alexsubALTlem4  23417  alexsubALT  23418  tsmsgsum  23506  tsmsres  23511  tsmsxplem1  23520  ustincl  23575  ustdiag  23576  ustinvel  23577  ustexhalf  23578  cfiluexsm  23658  psmet0  23677  prdsbl  23863  metss  23880  metcnp3  23912  isngp4  23984  nmoi  24108  mulc1cncf  24284  cncfco  24286  lebnumii  24345  iscfil3  24653  iscau2  24657  iscau4  24659  equivcfil  24679  equivcau  24680  lmcau  24693  ismbf  25008  ellimc3  25259  lhop1  25394  dvfsumlem4  25409  dvfsum2  25414  dgrco  25652  fta1  25684  aalioulem2  25709  aalioulem4  25711  ulmclm  25762  ulmshftlem  25764  ulmcaulem  25769  ulmcau  25770  ulmcn  25774  cxploglim  26343  ftalem3  26440  chtub  26576  dchrelbasd  26603  2sqlem6  26787  2sqlem10  26792  dchrisumlema  26852  dchrisumlem2  26854  dchrisumlem3  26855  dchrvmasumlem2  26862  pntpbnd1  26950  pntibnd  26957  pntleml  26975  nolt02o  27059  noresle  27061  nosupbnd1lem1  27072  nosupbnd1lem4  27075  nosupbnd2lem1  27079  nosupbnd2  27080  nocvxminlem  27139  madebdaylemold  27249  brbtwn2  27896  colinearalg  27901  axcontlem4  27958  usgruspgrb  28174  cusgredg  28414  cusgrres  28438  usgredgsscusgredg  28449  fusgrn0degnn0  28489  wlk1walk  28629  wlkres  28660  wlkp1lem6  28668  wlkdlem2  28673  upgrwlkdvdelem  28726  pthdlem2lem  28757  lfgrn1cycl  28792  wwlksnredwwlkn  28882  wwlksnextproplem2  28897  clwwlkccatlem  28975  clwlkclwwlkf1lem3  28992  clwwisshclwwslemlem  28999  clwwlkf1  29035  clwwlkext2edg  29042  3cyclfrgrrn1  29271  n4cyclfrgr  29277  frgrwopregasn  29302  frgrwopregbsn  29303  isgrpo  29481  blocnilem  29788  ip2eqi  29840  htthlem  29901  hial0  30086  hial02  30087  hial2eq  30090  ocorth  30275  h1de2i  30537  pjjsi  30684  lnopunilem1  30994  lnophmlem1  31000  nmcexi  31010  riesz4i  31047  mdi  31279  mdbr3  31281  mdbr4  31282  dmdi  31286  dmdbr3  31289  dmdbr4  31290  dmdi4  31291  mdslmd1i  31313  atss  31330  atom1d  31337  atmd  31383  sumdmdlem2  31403  cdj1i  31417  cdj3i  31425  fnpreimac  31629  nn0min  31758  archiabllem1a  32069  archiabllem2a  32072  archiabl  32076  isarchiofld  32152  crefi  32468  pcmplfin  32481  fmcncfil  32552  sigaclcu  32756  unelsiga  32773  sigapildsys  32801  ldgenpisys  32805  measvun  32848  carsgclctunlem2  32959  sibfima  32978  fnrelpredd  33733  pfxwlk  33757  derangenlem  33805  subfacp1lem6  33819  resconn  33880  cvmcov  33897  cvmliftlem3  33921  cvmliftphtlem  33951  satfdmfmla  34034  mclsax  34203  dfon2lem6  34402  fwddifnp1  34779  opnrebl2  34822  nn0prpwlem  34823  nn0prpw  34824  neibastop2lem  34861  neibastop2  34862  filnetlem4  34882  bj-mooreset  35602  bj-ismoored0  35606  dfgcd3  35824  fin2so  36094  poimirlem25  36132  poimirlem29  36136  poimir  36140  mbfresfi  36153  ftc1cnnclem  36178  seqpo  36235  incsequz  36236  mettrifi  36245  geomcau  36247  caushft  36249  sstotbnd2  36262  equivtotbnd  36266  totbndbnd  36277  ismtybndlem  36294  heibor1lem  36297  bfplem2  36311  opidonOLD  36340  exidu1  36344  rngoideu  36391  isdrngo2  36446  unichnidl  36519  lsat0cv  37524  lcvexchlem4  37528  lcvexchlem5  37529  eqlkr3  37592  lub0N  37680  glb0N  37684  cvrnbtwn  37762  ltrneq2  38640  trlval2  38655  lpolsatN  39980  lpolpolsatN  39981  hdmap14lem12  40371  isdomn4  40653  fsuppind  40794  nna4b4nsq  41027  incssnn0  41063  lnmlssfg  41436  unxpwdom3  41451  neik0pk1imk0  42393  ismnushort  42655  fnchoice  43308  monoordxrv  43791  monoord2xrv  43793  limcrecl  43944  fourierdlem54  44475  fourierdlem103  44524  fourierdlem104  44525  euoreqb  45415  smonoord  45637  iccpartlt  45690  iccpartgt  45693  iccpartdisj  45703  paireqne  45777  fmtnodvds  45810  perfectALTVlem2  45988  sbgoldbwt  46043  sbgoldbst  46044  sgoldbeven3prm  46049  mogoldbb  46051  nnsum4primesodd  46062  nnsum4primesoddALTV  46063  bgoldbnnsum3prm  46070  bgoldbtbndlem2  46072  bgoldbtbndlem3  46073  bgoldbtbndlem4  46074  bgoldbtbnd  46075  tgblthelfgott  46081  tgoldbach  46083  isomuspgrlem2c  46096  isomuspgrlem2d  46097  lcosslsp  46593  linindslinci  46603  lindslinindsimp1  46612  ldepsnlinclem1  46660  ldepsnlinclem2  46661  iscnrm3r  47055
  Copyright terms: Public domain W3C validator