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

Theorem nfv 1707
Description: If is not present in , then is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfv
Distinct variable group:   ,

Proof of Theorem nfv
StepHypRef Expression
1 ax-5 1704 . 2
21nfi 1623 1
Colors of variables: wff setvar class
Syntax hints:  F/wnf 1616
This theorem is referenced by:  nfvd  1708  nexdv  1884  dvelimhw  1955  19.21vOLD  1981  19.23vOLD  1982  pm11.53  1983  19.36vOLD  1984  19.36aivOLD  1985  19.12vv  1986  eeanv  1988  eeeanv  1989  spimv  2009  spimev  2010  chvarv  2014  cbvalv  2023  cbvexv  2024  cbvald  2025  cbval2  2027  cbvex2OLD  2029  cbval2v  2030  cbvex2v  2031  cbvaldva  2032  cbvexdva  2033  axc9lem2  2040  axc16i  2064  dvelimnf  2081  cleljustALT  2110  sbiedv  2152  equsb3lem  2175  equsb3  2176  equsb3ALT  2177  elsb3  2178  elsb4  2179  sbhb  2182  sbnf2  2183  sbcom2  2189  sbcom4  2190  dfsb7  2199  sbid2v  2201  sbel2x  2203  sbco4lem  2209  sbco4  2210  2sb8e  2211  exsb  2212  euf  2292  mo2  2293  nfeud2  2296  eubidv  2304  mobidv  2305  sb8eu  2318  sb8euOLD  2319  mo3OLD  2324  euexALT  2328  eu5OLD  2330  euorv  2332  sbmo  2335  mo4f  2336  mo4  2337  morimvOLD  2342  moanimv  2352  euanv  2355  mopickOLD  2357  moexexv  2364  2mo  2373  2moOLD  2374  2mos  2375  2eu4OLD  2381  2eu6  2383  2eu6OLD  2384  bm1.1  2440  bm1.1OLD  2441  cleqh  2572  eqsb3lem  2576  eqsb3  2577  clelsb3  2578  abbiOLD  2589  abbidv  2593  cbvabv  2600  clelab  2601  clelabOLD  2602  nfcjust  2606  nfcv  2619  nfeqd  2626  nfeld  2627  nfabd2  2640  dvelimdc  2642  cleqfOLD  2647  sbabel  2650  sbabelOLD  2651  r19.21vOLD  2863  ralimdvaOLD  2866  ralrimivOLD  2870  ralrimdvOLD  2874  ralbidvaOLD  2894  ralbidvOLD  2897  2ralbida  2898  2ralbidvaOLD  2900  reximdvaiOLD  2930  r19.23vOLD  2938  rexlimivOLD  2944  rexlimdvOLD  2948  rexbidvaALT  2966  rexbidvALT  2969  r19.29af  2997  r19.29an  2998  r19.29a  2999  r19.37v  3007  reean  3024  reeanv  3025  reubidva  3041  rmobidva  3046  cbvralf  3078  cbvreu  3082  cbvralv  3084  cbvrexv  3085  cbvreuv  3086  cbvrmov  3087  cbvralsv  3095  cbvrexsv  3096  sbralie  3097  cbvrab  3107  cbvrabv  3108  issetf  3114  ceqsalv  3137  ceqsralv  3138  ceqsexv  3146  ceqsex2  3147  ceqsex2v  3148  vtocld  3159  vtocl  3161  vtoclg  3167  vtocl2g  3171  vtoclga  3173  vtocl2gaf  3174  vtocl2ga  3175  vtocl3gaf  3176  vtocl3ga  3177  spcimdv  3191  spcgv  3194  spcegv  3195  rspct  3203  rspc  3204  rspce  3205  rspcv  3206  rspcev  3210  rspc2v  3219  eqvincf  3227  ceqsexgv  3232  elabgt  3243  elab  3246  elabg  3247  elab3g  3252  elrab3t  3256  elrab  3257  ralab2  3264  rexab2  3266  mob2  3279  mob  3281  reu2  3287  reu2eqd  3296  nfcdeq  3324  sbcco  3350  sbcco2  3351  cbvsbcv  3357  sbcieg  3360  sbcie2g  3361  sbcied  3364  elrabsf  3366  sbcbidv  3386  sbcg  3401  sbc2iegf  3402  sbc2ie  3403  rmo2  3427  rmo3  3429  nfcsb1d  3448  nfcsbd  3451  csbiebt  3454  csbied  3461  csbie2t  3463  cbvralcsf  3466  cbvreucsf  3468  cbvrabcsf  3469  cbvralv2  3470  cbvrexv2  3471  dfss2f  3494  uniiunlem  3587  rspn0  3797  csbeq2dv  3835  sbcnestg  3841  sbnfc2  3854  sbss  3939  nfifd  3969  rabsnifsb  4098  euabsn  4102  nfuni  4255  nfunid  4256  eluniab  4260  nfint  4296  elintab  4297  rabasiun  4334  iineq2dv  4353  disjiun  4442  disjxun  4450  opabbidv  4515  nfopab  4517  cbvopab  4520  cbvopabv  4521  cbvopab1  4522  cbvopab2  4523  cbvopab1s  4524  cbvopab1v  4525  mpteq12f  4528  mpteq2dva  4538  cbvmpt  4542  axrep1  4564  axrep2  4565  axrep3  4566  axrep4  4567  axrep5  4568  zfrepclf  4569  axsep  4572  zfnuleu  4578  reusv2lem2  4654  reusv2lem3  4655  reusv2lem4  4656  reusv2  4658  reusv3  4660  reusv6OLD  4663  alxfr  4665  ralxfrALT  4671  copsex2t  4739  copsex2g  4740  opelopabaf  4776  nfso  4811  pofun  4821  nffr  4858  opeliunxp  5056  opeliunxp2  5146  ralxpf  5154  dfdmf  5201  dfrnf  5246  elrnmpt1  5256  asymref2  5389  intirr  5390  nfiotad  5559  cbviota  5561  cbviotav  5562  sb8iota  5563  iota2d  5581  iota2  5582  dffun6f  5607  fun11  5658  imadif  5668  funimaexg  5670  isarep1  5672  isarep2  5673  fv3  5884  tz6.12f  5889  tz6.12c  5890  opabiotafun  5934  funfv2f  5942  fvmptdf  5967  fvmptdv  5968  fvmptt  5971  fvopab5  5979  eqfnfv2f  5985  ralrnmpt  6040  f1ompt  6053  ffnfv  6057  ffnfvf  6058  fmptco  6064  elabrex  6155  dff13f  6167  fliftfun  6210  cbvriota  6267  cbvriotav  6268  riota2  6280  riota5f  6282  oprabv  6345  nfoprab  6349  oprabbidv  6351  mpt2eq123  6356  cbvoprab1  6369  cbvoprab2  6370  cbvoprab12  6371  cbvoprab12v  6372  cbvoprab3  6373  cbvoprab3v  6374  cbvmpt2x  6375  ralrnmpt2  6417  ovmpt2dx  6429  ovmpt2df  6434  ovmpt2dv  6435  ov3  6439  ovmpt3rab1  6534  ofrfval2  6557  onminex  6642  tfis  6689  tfis2  6691  tfisi  6693  tfinds  6694  tfindes  6697  peano5  6723  findes  6730  fun11iun  6760  abrexex2g  6777  opabex3d  6778  opabex3  6779  abrexex2  6781  dfoprab4f  6858  fmpt2x  6866  offval22  6879  ovmptss  6881  tposoprab  7010  fvmpt2curryd  7019  nfrecs  7063  tfr3  7087  nfrdg  7099  tz7.48-1  7127  tz7.49  7129  eqerlem  7362  erovlem  7426  mptelixpg  7526  boxcutc  7532  dom2lem  7575  xpf1o  7699  mapxpen  7703  nneneq  7720  pssnn  7758  findcard2  7780  ac6sfi  7784  fiint  7817  indexfi  7848  wdom2d  8027  ixpiunwdom  8038  sucprcregOLD  8047  cantnflem1  8129  r1val1  8225  rankuni2b  8292  scottexs  8326  scott0s  8327  dfac8clem  8434  acni2  8448  aceq1  8519  dfac5lem5  8529  kmlem15  8565  infpssrlem4  8707  fin23lem27  8729  hsmexlem2  8828  hsmexlem4  8830  axcc3  8839  domtriomlem  8843  axdc3lem2  8852  axdc3lem4  8854  axdc4lem  8856  ac6num  8880  ac6c4  8882  zorn2lem4  8900  zorn2lem5  8901  iunfo  8935  iundom2g  8936  uniimadomf  8941  konigthlem  8964  axrepndlem2  8989  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem4  8998  axregndlem2  9001  axacndlem5  9010  zfcndrep  9013  zfcndinf  9017  pwfseqlem4a  9060  pwfseqlem4  9061  tskuni  9182  gruiin  9209  reclem2pr  9447  dedekind  9765  dedekindle  9766  fimaxre3  10517  uzindOLD  10982  nn0ind-raph  10989  uzind4s  11170  nnwof  11177  lbzbi  11199  fzrevral  11792  rabssnn0fi  12095  fsuppmapnn0fiublem  12096  fsuppmapnn0fiub  12097  fsuppmapnn0fiubex  12098  seqof2  12165  rlim2  13319  ello1mpt  13344  climeu  13378  o1compt  13410  summolem2a  13537  zsum  13540  sumss  13546  sumss2  13548  fsumcvg2  13549  fsum2dlem  13585  fsum00  13612  o1fsum  13627  nfcprod1  13717  nfcprod  13718  prodmolem2a  13741  zprod  13744  fprod  13748  fprodntriv  13749  prodss  13754  fprodn0  13783  fprod2dlem  13784  prmind2  14228  iserodd  14359  pcmpt  14411  pcmptdvds  14413  mreexexd  15045  catpropd  15104  invfuc  15343  natpropd  15345  fucpropd  15346  acsmapd  15808  gsumsnd  16979  gsumsnf  16980  gsumunsnfd  16983  gsummptf1o  16990  gsummpt1n0  16992  gsum2d2lem  17001  gsumcom2  17003  gsummptnn0fz  17014  gsummptnn0fzv  17015  dprdwdOLD2  17045  dprdwdOLD  17051  dprd2d2  17093  gsummoncoe1  18346  gsumply1eq  18347  mdetralt2  19111  mdetunilem2  19115  madugsum  19145  gsummatr01lem4  19160  cpmatmcllem  19219  pmatcollpwfi  19283  cayleyhamilton1  19393  neiptopnei  19633  neiptopreu  19634  neitr  19681  fiuncmp  19904  bwthOLD  19911  iunconlem  19928  iuncon  19929  2ndcdisj  19957  dissnlocfin  20030  elptr2  20075  ptbasfi  20082  ptcld  20114  ptcldmpt  20115  ptclsg  20116  ptcnplem  20122  ptcnp  20123  cnmpt11  20164  cnmpt21  20172  cnmptcom  20179  imasnopn  20191  imasncld  20192  imasncls  20193  xkocnv  20315  elmptrab  20328  isfildlem  20358  alexsubALTlem3  20549  cnextfvval  20565  utopsnneiplem  20750  isucn2  20782  cfilucfilOLD  21072  cfilucfil  21073  blval2  21078  restmetu  21090  ovoliunlem3  21915  ovoliun  21916  ovoliun2  21917  ovoliunnul  21918  finiunmbl  21954  volfiniun  21957  iundisj  21958  iunmbl  21963  voliun  21964  iunmbl2  21967  mbfeqalem  22049  mbfsup  22071  mbfinf  22072  mbflim  22075  itg2splitlem  22155  itg2split  22156  isibl2  22173  cbvitg  22182  itgeqa  22220  itgss3  22221  itgfsum  22233  itgabs  22241  itggt0  22248  itgcn  22249  limcmpt  22287  limciun  22298  dvmptfsum  22376  dvlipcn  22395  dvfsumlem2  22428  dvfsumlem4  22430  dvfsumrlim  22432  dvfsum2  22435  itgsubst  22450  coeeq2  22639  dgrle  22640  ulmss  22792  leibpi  23273  rlimcnp  23295  rlimcnp2  23296  o1cxp  23304  fsumdvdscom  23461  lgseisenlem2  23625  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  istrkg2ld  23858  mptelee  24198  ex-natded9.26  25140  isch3  26159  atom1d  27272  chirred  27314  spc2ed  27372  19.9d2r  27378  clelsb3f  27379  mo5f  27383  rmoeq  27386  rmo4fOLD  27395  rmo4f  27396  foresf1o  27403  elabreximdv  27409  rabss3d  27412  iuninc  27428  cbvdisjf  27434  disjorf  27440  disjabrex  27443  iundisjf  27448  disjunsn  27453  dfrel4  27454  dfimafnf  27473  suppss2f  27477  fimarab  27483  cbvmptf  27494  feqmptdf  27501  fmptcof2  27502  ofpreima  27507  funcnvmptOLD  27509  funcnv5mpt  27511  funcnv4mpt  27512  cnvoprab  27546  f1od2  27547  fpwrelmap  27556  xrofsup  27582  iundisjfi  27601  nnindf  27610  nn0min  27611  2sqmo  27637  isarchiofld  27807  reff  27842  locfinreflem  27843  cmpcref  27853  ordtconlem1  27906  qqhval2  27963  esumeq12dva  28045  esumeq2dv  28051  esumc  28062  esumadd  28064  gsumesum  28067  esumlub  28068  esumpr  28073  esumfzf  28075  esumfsup  28076  esumpcvgval  28084  esumpmono  28085  esumcocn  28086  hasheuni  28091  esumcvg  28092  measvunilem  28183  measvunilem0  28184  measvuni  28185  measiuns  28188  measiun  28189  measinblem  28191  voliune  28201  volfiniune  28202  volmeas  28203  ddemeas  28208  oms0  28266  eulerpartlemgvv  28315  dstrvprob  28410  ballotlemodife  28436  lgamgulmlem2  28572  lgamgulmlem6  28576  cvmcov  28708  untsucf  29082  mpteq12d  29202  setinds2  29212  dfon2lem1  29215  dfon2lem3  29217  wfisg  29289  wfis2g  29293  trpredmintr  29314  frinsg  29325  frins2g  29329  frins2  29330  nfwrecs  29338  wl-equsb3  30004  wl-sb8eut  30022  ptrest  30048  heicant  30049  mbfposadd  30062  itgabsnc  30084  itggt0cn  30087  ftc1anclem5  30094  finminlem  30136  upixp  30220  indexa  30224  indexdom  30225  filbcmb  30231  sdclem2  30235  sdclem1  30236  fdc1  30239  totbndbnd  30285  sbcalf  30517  sbcexf  30518  scottexf  30576  scott0f  30577  prtlem5  30597  mzpexpmpt  30677  eq0rabdioph  30710  rexrabdioph  30727  rexfrabdioph  30728  elnn0rabdioph  30736  dvdsrabdioph  30743  fphpd  30750  monotuz  30877  monotoddzz  30879  oddcomabszz  30880  setindtr  30966  dford4  30971  wdom2d2  30977  aomclem6  31005  aomclem8  31007  flcidc  31123  areaquad  31184  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  aaanv  31294  pm11.57  31295  pm11.58  31296  pm11.59  31297  pm11.71  31303  pm13.192  31317  pm14.12  31328  evth2f  31390  elunif  31391  fvelrnbf  31393  evthf  31402  fnchoice  31404  sumpair  31410  rfcnnnub  31411  refsum2cn  31413  elabrexg  31430  suprnmpt  31451  upbdrech  31505  ssfiunibd  31509  iccshift  31558  iooshift  31562  fsumclf  31567  fsumsplitf  31568  fsummulc1f  31569  fsumnncl  31572  fsumsplit1  31573  fmul01  31574  fmuldfeqlem1  31576  fmuldfeq  31577  fmul01lt1lem1  31578  fmul01lt1lem2  31579  fmul01lt1  31580  infrglb  31584  fprodsplitf  31589  fprodsplit1f  31593  fprodsplit1  31599  fprodexp  31600  fprodabs2  31602  fprodle  31604  mccllem  31605  mccl  31606  climexp  31611  climsuse  31614  climrecf  31615  climinff  31617  climaddf  31621  mullimc  31622  ellimcabssub0  31623  islptre  31625  climf  31628  mullimcf  31629  rexlim2d  31631  idlimc  31632  limcperiod  31634  limcrecl  31635  sumnnodd  31636  islpcn  31645  limsupre  31647  limcleqr  31650  neglimc  31653  addlimc  31654  0ellimcdiv  31655  limclner  31657  cncfshift  31676  icccncfext  31690  cncficcgt0  31691  cncfiooicclem1  31696  cncfiooicc  31697  cncfioobd  31700  fprodcncf  31704  dvmptmulf  31734  dvnmptdivc  31735  dvnmul  31740  dvmptfprodlem  31741  dvmptfprod  31742  dvnprodlem1  31743  dvnprodlem2  31744  iblsplitf  31769  iblspltprt  31772  itgioocnicc  31776  iblcncfioo  31777  itgspltprt  31778  itgperiod  31780  stoweidlem3  31785  stoweidlem14  31796  stoweidlem17  31799  stoweidlem19  31801  stoweidlem20  31802  stoweidlem26  31808  stoweidlem27  31809  stoweidlem28  31810  stoweidlem29  31811  stoweidlem31  31813  stoweidlem34  31816  stoweidlem35  31817  stoweidlem36  31818  stoweidlem39  31821  stoweidlem42  31824  stoweidlem43  31825  stoweidlem44  31826  stoweidlem46  31828  stoweidlem48  31830  stoweidlem49  31831  stoweidlem50  31832  stoweidlem51  31833  stoweidlem52  31834  stoweidlem53  31835  stoweidlem54  31836  stoweidlem56  31838  stoweidlem57  31839  stoweidlem59  31841  stoweidlem60  31842  stoweidlem61  31843  stoweidlem62  31844  stoweid  31845  wallispilem3  31849  stirlinglem13  31868  stirling  31871  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem31  31920  fourierdlem39  31928  fourierdlem48  31937  fourierdlem51  31940  fourierdlem53  31942  fourierdlem68  31957  fourierdlem69  31958  fourierdlem71  31960  fourierdlem73  31962  fourierdlem77  31966  fourierdlem80  31969  fourierdlem81  31970  fourierdlem82  31971  fourierdlem83  31972  fourierdlem86  31975  fourierdlem87  31976  fourierdlem89  31978  fourierdlem91  31980  fourierdlem93  31982  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem113  32002  elaa2  32017  etransclem18  32035  etransclem22  32039  etransclem23  32040  etransclem32  32049  etransclem35  32052  etransclem44  32061  etransclem46  32063  etransclem48  32065  rexsb  32173  rmoanim  32184  2reu4a  32194  ffnafv  32256  initoeu2  32622  2zrngagrp  32749  2zrngmmgm  32752  opeliun2xp  32922  cbvmpt2x2  32925  ovmpt2rdx  32929  aacllem  33216  ssralv2  33301  tratrb  33307  iunconlem2  33735  bnj919  33825  bnj1146  33850  bnj1379  33889  bnj1385  33891  bnj1400  33894  bnj1476  33905  bnj1534  33911  bnj1542  33915  bnj110  33916  bnj121  33928  bnj124  33929  bnj130  33932  bnj207  33939  bnj571  33964  bnj605  33965  bnj580  33971  bnj607  33974  bnj611  33976  bnj873  33982  bnj849  33983  bnj900  33987  bnj916  33991  bnj1000  33999  bnj964  34001  bnj981  34008  bnj985  34011  bnj1014  34018  bnj1123  34042  bnj1128  34046  bnj1228  34067  bnj1204  34068  bnj1279  34074  bnj1307  34079  bnj1321  34083  bnj1388  34089  bnj1398  34090  bnj1408  34092  bnj1417  34097  bnj1444  34099  bnj1445  34100  bnj1446  34101  bnj1449  34104  bnj1467  34110  bnj1489  34112  bnj1312  34114  bnj1497  34116  bnj1518  34120  bnj1525  34125  bnj1529  34126  bj-nexdvt  34251  bj-spimvv  34282  bj-spimevv  34283  bj-chvarvv  34287  bj-cbv3v2  34289  bj-cbvalvv  34298  bj-cbvexvv  34299  bj-cbvaldv  34300  bj-cbval2v  34302  bj-cbval2vv  34304  bj-cbvex2vv  34305  bj-cbvaldvav  34306  bj-cbvexdvav  34307  bj-drnf2v  34329  bj-abbi  34361  bj-abbidv  34365  bj-axrep1  34374  bj-axrep2  34375  bj-axrep3  34376  bj-axrep4  34377  bj-axrep5  34378  bj-axsep  34379  ax11-pm2  34409  bj-clelsb3  34424  bj-nfcjust  34426  bj-ceqsalv  34459  bj-vtocl  34481  bj-inrab2  34496  fsumshftd  34682  fsumshftdOLD  34683  riotasv2d  34688  riotasv2s  34689  riotasv3d  34691  glbconxN  35102  pmapglbx  35493  pmapglb2xN  35496  cdleme26ee  36086  cdleme31sn  36106  cdleme31sn1  36107  cdlemefr29exN  36128  cdlemefs32sn1aw  36140  cdleme43fsv1snlem  36146  cdleme41sn3a  36159  cdleme32fva  36163  cdleme32d  36170  cdleme32f  36172  cdleme40m  36193  cdleme40n  36194  cdleme42b  36204  cdlemk36  36639  cdlemk38  36641  cdlemkid  36662  cdlemk19x  36669  cdlemk11t  36672  dihvalcqpre  36962  mapdheq  37455  hdmap1eq  37529  hdmapval2lem  37561  cotr2g  37786  frege70  37961  frege72  37963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-nf 1617
  Copyright terms: Public domain W3C validator