MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvralv Unicode version

Theorem cbvralv 3084
Description: Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.)
Hypothesis
Ref Expression
cbvralv.1
Assertion
Ref Expression
cbvralv
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem cbvralv
StepHypRef Expression
1 nfv 1707 . 2
2 nfv 1707 . 2
3 cbvralv.1 . 2
41, 2, 3cbvral 3080 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wral 2807
This theorem is referenced by:  cbvral2v  3092  cbvral3v  3094  reu7  3294  disjxun  4450  reusv3i  4659  wereu2  4881  cnvpo  5550  f1mpt  6169  grprinvlem  6513  grprinvd  6514  dfwe2  6617  tfinds  6694  tfrlem1  7064  tfrlem12  7077  rdglem1  7100  tz7.48lem  7125  nneneq  7720  marypha1lem  7913  supub  7939  suplub  7940  supmaxlemOLD  7945  ordtypecbv  7963  ordtypelem3  7966  ordtypelem9  7972  wemaplem1  7992  brwdom3  8029  tcrank  8323  infxpenc2  8420  infxpenc2OLD  8424  aceq1  8519  aceq2  8521  dfac5  8530  dfac9  8537  dfac12lem3  8546  kmlem12  8562  kmlem14  8564  cofsmo  8670  infpssrlem4  8707  isfin3ds  8730  isf32lem2  8755  isf32lem11  8764  isf33lem  8767  domtriomlem  8843  axdc3  8855  zorn2lem7  8903  zorn2g  8904  fpwwe2cbv  9029  fpwwecbv  9043  pwfseq  9063  axgroth6  9227  dedekind  9765  suprleub  10532  infmrgelb  10548  nnsub  10599  uzwo  11173  uzwoOLD  11174  ublbneg  11195  zsupss  11200  xrub  11532  fsuppmapnn0fiubex  12098  monoord2  12138  faclbnd4lem4  12374  bccl  12400  hashbc  12502  wrdind  12702  wrd2ind  12703  reuccats1  12706  cau3lem  13187  climmpt2  13396  caucvgrlem  13495  caurcvg2  13500  caucvgb  13502  fsum0diag2  13598  incexclem  13648  cvgrat  13692  mertenslem2  13694  mertens  13695  sqrt2irr  13982  gcdcllem1  14149  prmind2  14228  prmpwdvds  14422  prmreclem5  14438  prmreclem6  14439  vdwlem7  14505  vdwlem10  14508  vdwlem13  14511  vdwnn  14516  ramcl  14547  isacs2  15050  catpropd  15104  gsumvalx  15897  mrcmndind  15997  issubg4  16220  isnsg2  16231  elnmz  16240  gsmsymgreqlem2  16456  psgnunilem5  16519  psgnunilem3  16521  efgsdm  16748  gsummptnn0fzfv  17016  pgpfac1lem5  17130  pgpfac1  17131  pgpfac  17135  ablfaclem3  17138  lbsextg  17808  evlslem2  18180  mpfind  18205  cply1mul  18335  mdetuni0  19123  m2cpminvid2lem  19255  mp2pm2mplem4  19310  chcoeffeqlem  19386  cayhamlem3  19388  elcls3  19584  isclo2  19589  neiptopnei  19633  tgcn  19753  subbascn  19755  txcmplem2  20143  kqfvima  20231  kqt0lem  20237  isr0  20238  r0cld  20239  regr1lem2  20241  fbun  20341  flftg  20497  fclsbas  20522  alexsubALTlem2  20548  alexsubALTlem4  20550  ptcmplem4  20555  tsmsxplem1  20655  tsmsxp  20657  ustuqtop  20749  utopsnneip  20751  prdsxmslem2  21032  iscau4  21718  caucfil  21722  iscmet3  21732  bcthlem5  21767  bcth  21768  ovolicc2lem5  21932  uniioombllem6  21997  vitali  22022  ismbf3d  22061  itg1climres  22121  itg2seq  22149  itg2monolem1  22157  itg2mono  22160  rolle  22391  dvlipcn  22395  dvivthlem1  22409  ply1divex  22537  fta1g  22568  dgrco  22672  plydivex  22693  fta1  22704  vieta1  22708  ulmcaulem  22789  ulmcau  22790  abelthlem8  22834  wilth  23345  fta  23353  dchrelbas3  23513  2sqlem6  23644  2sqlem10  23649  dchrisumlem3  23676  dchrisum  23677  dchrmusumlema  23678  dchrvmasumlema  23685  dchrisum0lema  23699  pntibndlem3  23777  pntlem3  23794  pntleml  23796  pnt3  23797  ostth2lem2  23819  ostth  23824  axcontlem1  24267  axcontlem6  24272  cusgrafilem2  24480  usg2wlkeq  24708  grpoideu  25211  ubthlem3  25788  adjsym  26752  lnopunilem1  26929  elunop2  26932  lnophm  26938  cnlnadjlem5  26990  mdbr3  27216  mdbr4  27217  dmdbr3  27224  dmdbr4  27225  mddmd2  27228  toslublem  27655  tosglblem  27657  archiabl  27742  isarchiofld  27807  qtophaus  27839  lmdvg  27935  esumcvg  28092  eulerpartlemsv3  28300  eulerpartlemgvv  28315  signstfvneq0  28529  derangenlem  28615  subfacp1lem6  28629  subfacp1  28630  rescon  28691  cvmscbv  28703  untangtr  29086  dfon2lem3  29217  dfon2lem7  29221  cbvsetlike  29261  wfrlem1  29343  frrlem1  29387  heicant  30049  mblfinlem2  30052  ovoliunnfl  30056  voliunnfl  30058  mbfresfi  30061  nn0prpwlem  30140  neibastop3  30180  fnemeet2  30185  upixp  30220  sdclem2  30235  fdc  30238  mettrifi  30250  heiborlem5  30311  heiborlem10  30316  heibor  30317  bfp  30320  mzpclval  30657  dford3lem1  30968  fnwe2lem1  30996  aomclem3  31002  aomclem4  31003  aomclem8  31007  dfac11  31008  hbtlem5  31077  fnchoice  31404  cncmpmax  31407  mccl  31606  climsuse  31614  limsupre  31647  dvbdfbdioolem2  31726  dvbdfbdioo  31727  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnprodlem3  31745  stoweidlem7  31789  stoweidlem15  31797  stoweidlem35  31817  wallispilem3  31849  fourierdlem68  31957  fourierdlem71  31960  fourierdlem73  31962  fourierdlem87  31976  fourierdlem100  31989  fourierdlem103  31992  fourierdlem104  31993  fourierdlem107  31996  fourierdlem109  31998  fourierdlem112  32001  etransc  32066  bnj1185  33852  bnj1379  33889  bnj222  33941  bnj517  33943  bnj1450  34106  bnj1452  34108  bnj1463  34111  cdleme25cv  36084  cdleme40v  36195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812
  Copyright terms: Public domain W3C validator