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

Theorem rspcv 3498
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
Hypothesis
Ref Expression
rspcv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspcv (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcv
StepHypRef Expression
1 nfv 2005 . 2 𝑥𝜓
2 rspcv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2rspc 3496 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wcel 2156  wral 3096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-v 3393
This theorem is referenced by:  rspccv  3499  rspcva  3500  rspccva  3501  rspcdva  3508  rspc3v  3518  rr19.3v  3540  rr19.28v  3541  rspsbc  3713  intmin  4689  ralxfrALT  5084  somo  5266  fr2nr  5289  weniso  6828  fr3nr  7209  limuni3  7282  tfinds  7289  funcnvuni  7349  suppfnss  7554  suppfnssOLD  7555  onnseq  7677  smo11  7697  tfrlem9  7717  tz7.49  7776  omeulem1  7899  oeordi  7904  nneneq  8382  frfi  8444  unblem2  8452  unbnn2  8456  xpfi  8470  ordiso2  8659  cantnflem1  8833  rankunb  8960  tcrank  8994  carduni  9090  dfac8alem  9135  alephinit  9201  aceq3lem  9226  dfac5  9234  dfac12r  9253  dfac12k  9254  pwsdompw  9311  cflm  9357  isf32lem1  9460  isf32lem2  9461  isf34lem4  9484  hsmexlem4  9536  axcc3  9545  domtriomlem  9549  axdc3lem2  9558  axdc4lem  9562  axcclem  9564  axdclem  9626  alephval2  9679  winainflem  9800  eltskm  9950  squeeze0  11211  fiminre  11257  lbreu  11258  nnsub  11345  ublbneg  11992  zmax  12004  zbtwnre  12005  xrub  12360  infmremnf  12391  infmrp1  12392  fzrevral  12648  axdc4uzlem  13006  faclbnd4lem4  13303  ccatalpha  13590  wrdind  13700  wrd2ind  13701  reuccats1lem  13703  recan  14299  cau3lem  14317  caubnd2  14320  climrlim2  14501  climshftlem  14528  rlimcld2  14532  subcn2  14548  isercoll  14621  climcau  14624  serf0  14634  iseralt  14638  isumrpcl  14797  clim2prod  14841  ntrivcvgfvn0  14852  sqrt2irr  15199  ndvdssub  15352  dfgcd2  15482  lcmf  15565  lcmfunsnlem1  15569  lcmfunsnlem2lem1  15570  lcmfunsnlem2lem2  15571  lcmfdvds  15574  lcmfdvdsb  15575  lcmfunsn  15576  coprmgcdb  15581  coprmdvds1  15584  coprmprod  15593  coprmproddvdslem  15594  nprm  15619  dvdsprm  15632  coprm  15640  pcmpt  15813  pcmptdvds  15815  pcfac  15820  prmpwdvds  15825  unbenlem  15829  vdwlem10  15911  vdwlem13  15914  vdwnnlem1  15916  prmdvdsprmop  15964  prmgaplem7  15978  catideu  16540  initoid  16859  termoid  16860  initoeu1  16865  termoeu1  16872  isdrs2  17144  lublecllem  17193  lubun  17328  sgrp2rid2ex  17619  dfgrp2  17652  grpidinv2  17679  dfgrp3lem  17718  issubg4  17815  efgi  18333  efgi2  18339  dprdss  18630  srgrz  18728  srglz  18729  srgisid  18730  f1rhm0to0ALT  18945  islmodd  19073  rmodislmod  19135  islmhm2  19245  rrgeq0i  19498  mvrf1  19634  cply1mul  19872  ip2eq  20208  isclo2  21106  cnpnei  21282  cncls  21292  lmss  21316  cnt0  21364  isnrm2  21376  isreg2  21395  tgcmp  21418  uncmp  21420  dfconn2  21436  1stcclb  21461  2ndcctbss  21472  comppfsc  21549  kgencn2  21574  ptpjpre1  21588  txlm  21665  kqfvima  21747  kqt0lem  21753  isr0  21754  nrmr0reg  21766  fgss2  21891  isufil2  21925  cfinufil  21945  flimopn  21992  fbflim2  21994  flfneii  22009  cnpflf  22018  fclssscls  22035  fclsnei  22036  fclsrest  22041  flimfnfcls  22045  fclscmp  22047  isfcf  22051  fcfnei  22052  alexsubALTlem3  22066  alexsubALTlem4  22067  alexsubALT  22068  tsmsgsum  22155  tsmsres  22160  tsmsxplem1  22169  ustincl  22224  ustdiag  22225  ustinvel  22226  ustexhalf  22227  cfiluexsm  22307  psmet0  22326  prdsbl  22509  metss  22526  metcnp3  22558  isngp4  22629  nmoi  22745  mulc1cncf  22921  cncfco  22923  lebnumii  22978  iscfil3  23283  iscau2  23287  iscau4  23289  equivcfil  23309  equivcau  23310  lmcau  23323  ismbf  23609  ellimc3  23857  lhop1  23991  dvfsumlem4  24006  dvfsum2  24011  dgrco  24245  fta1  24277  aalioulem2  24302  aalioulem4  24304  ulmclm  24355  ulmshftlem  24357  ulmcaulem  24362  ulmcau  24363  ulmcn  24367  cxploglim  24918  ftalem3  25015  chtub  25151  dchrelbasd  25178  2sqlem6  25362  2sqlem10  25367  dchrisumlema  25391  dchrisumlem2  25393  dchrisumlem3  25394  dchrvmasumlem2  25401  pntpbnd1  25489  pntibnd  25496  pntleml  25514  brbtwn2  25999  colinearalg  26004  axcontlem4  26061  usgruspgrb  26291  cusgredg  26548  cusgrres  26572  usgredgsscusgredg  26583  fusgrn0degnn0  26623  wlk1walk  26763  wlkres  26795  wlkp1lem6  26803  wlkdlem2  26808  upgrwlkdvdelem  26860  pthdlem2lem  26891  lfgrn1cycl  26926  wwlksnredwwlkn  27032  wwlksnextproplem2  27048  clwwlkccatlem  27132  clwlkclwwlkf1lem3  27149  clwwisshclwwslemlem  27156  clwwlkf1  27198  clwwlkext2edg  27206  clwlksf1clwwlklemOLD  27242  rspc2vd  27440  3cyclfrgrrn1  27460  n4cyclfrgr  27466  frgrwopregasn  27491  frgrwopregbsn  27492  isgrpo  27680  blocnilem  27987  ip2eqi  28040  htthlem  28102  hial0  28287  hial02  28288  hial2eq  28291  ocorth  28478  h1de2i  28740  pjjsi  28887  lnopunilem1  29197  lnophmlem1  29203  nmcexi  29213  riesz4i  29250  mdi  29482  mdbr3  29484  mdbr4  29485  dmdi  29489  dmdbr3  29492  dmdbr4  29493  dmdi4  29494  mdslmd1i  29516  atss  29533  atom1d  29540  atmd  29586  sumdmdlem2  29606  cdj1i  29620  cdj3i  29628  nn0min  29894  archiabllem1a  30070  archiabllem2a  30073  archiabl  30077  isarchiofld  30142  crefi  30239  pcmplfin  30252  fmcncfil  30302  sigaclcu  30505  unelsiga  30522  sigapildsys  30550  ldgenpisys  30554  measvun  30597  mbfmcnvima  30644  carsgclctunlem2  30706  sibfima  30725  derangenlem  31476  subfacp1lem5  31489  subfacp1lem6  31490  resconn  31551  cvmcov  31568  cvmliftlem3  31592  cvmliftphtlem  31622  mclsax  31789  dfon2lem6  32013  poseq  32074  soseq  32075  nolt02o  32166  noresle  32167  noprefixmo  32169  nosupbnd1lem1  32175  nosupbnd1lem4  32178  nosupbnd2lem1  32182  nosupbnd2  32183  nocvxminlem  32214  fwddifnp1  32593  opnrebl2  32637  nn0prpwlem  32638  nn0prpw  32639  neibastop2lem  32676  neibastop2  32677  filnetlem4  32697  bj-mooreset  33367  bj-ismoored0  33372  bj-ismoored  33373  dfgcd3  33487  fin2so  33709  poimirlem25  33747  poimirlem29  33751  poimir  33755  mbfresfi  33768  ftc1cnnclem  33795  seqpo  33854  incsequz  33855  mettrifi  33864  geomcau  33866  caushft  33868  sstotbnd2  33884  equivtotbnd  33888  totbndbnd  33899  ismtybndlem  33916  heibor1lem  33919  bfplem2  33933  opidonOLD  33962  exidu1  33966  rngoideu  34013  isdrngo2  34068  unichnidl  34141  lsat0cv  34813  lcvexchlem4  34817  lcvexchlem5  34818  eqlkr3  34881  lub0N  34969  glb0N  34973  cvrnbtwn  35051  ltrneq2  35928  trlval2  35944  lpolsatN  37269  lpolpolsatN  37270  hdmap14lem12  37660  incssnn0  37776  lnmlssfg  38151  unxpwdom3  38166  neik0pk1imk0  38845  fnchoice  39682  monoordxrv  40191  monoord2xrv  40193  limcrecl  40341  fourierdlem54  40856  fourierdlem103  40905  fourierdlem104  40906  smonoord  41916  iccpartlt  41935  iccpartgt  41938  iccpartdisj  41948  reuccatpfxs1lem  42008  fmtnodvds  42031  perfectALTVlem2  42206  sbgoldbwt  42240  sbgoldbst  42241  sgoldbeven3prm  42246  mogoldbb  42248  nnsum4primesodd  42259  nnsum4primesoddALTV  42260  bgoldbnnsum3prm  42267  bgoldbtbndlem2  42269  bgoldbtbndlem3  42270  bgoldbtbndlem4  42271  bgoldbtbnd  42272  tgblthelfgott  42278  tgoldbach  42280  lcosslsp  42795  linindslinci  42805  lindslinindsimp1  42814  ldepsnlinclem1  42862  ldepsnlinclem2  42863
  Copyright terms: Public domain W3C validator