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

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

Proof of Theorem nfv
StepHypRef Expression
1 ax-5 1669 . 2  |-  ( ph  ->  A. x ph )
21nfi 1599 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-5 1669
This theorem depends on definitions:  df-bi 185  df-nf 1593
This theorem is referenced by:  nfvd  1673  dvelimhw  1879  19.21v  1907  19.23v  1908  pm11.53  1910  19.27v  1911  19.28v  1912  19.36v  1913  19.36aiv  1914  19.12vv  1915  19.37v  1916  19.41v  1918  19.42v  1922  eeanv  1930  eeeanv  1931  nexdv  1933  spimv  1952  spimev  1953  chvarv  1957  cbvalv  1970  cbvexv  1971  cbvald  1972  cbval2  1974  cbvex2OLD  1976  cbval2v  1977  cbvex2v  1978  cbvaldva  1979  cbvexdva  1980  axc9lem2  1987  axc16i  2011  dvelimnf  2030  cleljustALT  2057  sbiedv  2102  axc16ALT2  2104  equsb3lem  2138  equsb3  2139  equsb3ALT  2140  elsb3  2141  elsb4  2142  sbhb  2145  sbnf2  2146  sbnf2OLD  2147  sbcom2  2153  sbcom4  2155  dfsb7  2167  sbid2v  2169  sbel2x  2171  sbco4lem  2180  sbco4  2181  exsb  2182  2exsb  2183  euf  2261  eufOLD  2262  mo2  2263  nfeud2  2266  eubidv  2274  mobidv  2275  nfeud2OLD  2278  sb8eu  2289  sb8euOLD  2290  mo3  2292  mo3OLD  2293  moOLD  2300  euexOLD  2301  eu5OLD  2304  euorv  2306  sbmo  2310  mo4f  2311  mo4  2312  morimvOLD  2319  moanimOLD  2330  moanimv  2331  euanv  2335  mopick  2336  mopickOLD  2337  moexexv  2347  2mo  2355  2moOLD  2356  2mos  2357  2eu4  2361  2eu6  2363  bm1.1  2418  eqsb3lem  2533  eqsb3  2534  clelsb3  2535  abbi  2543  abbidv  2547  cbvabv  2552  clelab  2553  nfcjust  2557  nfcv  2569  nfeqd  2583  nfeld  2584  nfabd2  2587  dvelimdc  2589  cleqf  2593  sbabel  2595  ralbidva  2721  rexbidva  2722  ralbidv  2725  rexbidv  2726  2ralbida  2744  2ralbidva  2745  ralimdva  2784  ralrimiv  2788  r19.21v  2793  ralrimdv  2795  reximdvai  2816  r19.23v  2823  rexlimiv  2825  rexlimdv  2830  r19.29af  2851  r19.29a  2852  r19.37av  2860  r19.41v  2863  reean  2877  reeanv  2878  reubidva  2894  rmobidva  2899  cbvralf  2931  cbvreu  2935  cbvralv  2937  cbvrexv  2938  cbvreuv  2939  cbvrmov  2940  cbvralsv  2948  cbvrexsv  2949  sbralie  2950  cbvrab  2960  cbvrabv  2961  issetf  2967  ceqsalv  2989  ceqsralv  2990  ceqsexv  2998  ceqsex2  2999  ceqsex2v  3000  vtocld  3011  vtocl  3013  vtoclg  3019  vtocl2g  3023  vtoclga  3025  vtocl2gaf  3026  vtocl2ga  3027  vtocl3gaf  3028  vtocl3ga  3029  spcimdv  3043  spcgv  3046  spcegv  3047  rspct  3055  rspc  3056  rspce  3057  rspcv  3058  rspcev  3062  rspc2v  3068  eqvincf  3076  ceqsexgv  3081  elabgt  3092  elab  3095  elabg  3096  elab3g  3101  elrab3t  3105  elrab  3106  ralab2  3113  rexab2  3115  mob2  3128  mob  3130  reu2  3136  nfcdeq  3172  sbcco  3197  sbcco2  3198  cbvsbcv  3204  sbcieg  3207  sbcie2g  3208  sbcied  3211  elrabsf  3213  sbcbidv  3233  sbcg  3248  sbc2iegf  3249  sbc2ie  3250  rmo2  3271  rmo3  3273  nfcsb1d  3290  nfcsbd  3293  csbiebt  3296  csbied  3302  csbie2t  3304  cbvralcsf  3307  cbvreucsf  3309  cbvrabcsf  3310  cbvralv2  3311  cbvrexv2  3312  dfss2f  3335  uniiunlem  3428  rspn0  3637  csbeq2dv  3675  sbcnestg  3681  sbnfc2  3694  sbss  3777  nfifd  3805  rabsnifsb  3931  euabsn  3935  nfuni  4085  nfunid  4086  eluniab  4090  nfint  4126  elintab  4127  iineq2dv  4181  disjiun  4270  disjxun  4278  opabbidv  4343  nfopab  4345  cbvopab  4348  cbvopabv  4349  cbvopab1  4350  cbvopab2  4351  cbvopab1s  4352  cbvopab1v  4353  mpteq12f  4356  mpteq2dva  4366  cbvmpt  4370  axrep1  4392  axrep2  4393  axrep3  4394  axrep4  4395  axrep5  4396  zfrepclf  4397  axsep  4400  zfnuleu  4406  reusv2lem2  4482  reusv2lem3  4483  reusv2lem4  4484  reusv2  4486  reusv3  4488  reusv6OLD  4491  alxfr  4493  ralxfrALT  4499  copsex2t  4566  copsex2g  4567  opelopabaf  4601  nfso  4634  pofun  4644  nffr  4681  opeliunxp  4877  opeliunxp2  4965  ralxpf  4973  dfdmf  5020  dfrnf  5065  elrnmpt1  5075  asymref2  5203  intirr  5204  nfiotad  5372  cbviota  5374  cbviotav  5375  sb8iota  5376  iota2d  5394  iota2  5395  dffun6f  5420  fun11  5471  imadif  5481  funimaexg  5483  isarep1  5485  isarep2  5486  fv3  5691  tz6.12f  5696  tz6.12c  5697  opabiotafun  5740  funfv2f  5748  fvmptdf  5773  fvmptdv  5774  fvmptt  5777  fvopab5  5783  eqfnfv2f  5789  ralrnmpt  5840  f1ompt  5853  ffnfv  5856  ffnfvf  5857  fmptco  5863  elabrex  5947  dff13f  5960  fliftfun  5992  cbvriota  6050  cbvriotav  6051  riota2  6063  riota5f  6065  nfoprab  6127  oprabbidv  6129  mpt2eq123  6134  cbvoprab1  6147  cbvoprab2  6148  cbvoprab12  6149  cbvoprab12v  6150  cbvoprab3  6151  cbvoprab3v  6152  cbvmpt2x  6153  ralrnmpt2  6194  ovmpt2dx  6206  ovmpt2df  6211  ovmpt2dv  6212  ov3  6216  ofrfval2  6326  onminex  6407  tfis  6454  tfis2  6456  tfisi  6458  tfinds  6459  tfindes  6462  peano5  6488  findes  6495  fun11iun  6526  abrexex2g  6543  opabex3d  6544  opabex3  6545  abrexex2  6547  dfoprab4f  6621  fmpt2x  6629  offval22  6641  ovmptss  6643  tposoprab  6770  nfrecs  6820  tfr3  6844  nfrdg  6856  tz7.48-1  6884  tz7.49  6886  eqerlem  7121  erovlem  7184  mptelixpg  7288  boxcutc  7294  dom2lem  7337  xpf1o  7461  mapxpen  7465  nneneq  7482  pssnn  7519  findcard2  7540  ac6sfi  7544  fiint  7576  indexfi  7607  wdom2d  7783  ixpiunwdom  7794  sucprcregOLD  7803  cantnflem1  7885  r1val1  7981  rankuni2b  8048  scottexs  8082  scott0s  8083  dfac8clem  8190  acni2  8204  aceq1  8275  dfac5lem5  8285  kmlem15  8321  infpssrlem4  8463  fin23lem27  8485  hsmexlem2  8584  hsmexlem4  8586  axcc3  8595  domtriomlem  8599  axdc3lem2  8608  axdc3lem4  8610  axdc4lem  8612  ac6num  8636  ac6c4  8638  zorn2lem4  8656  zorn2lem5  8657  iunfo  8691  iundom2g  8692  uniimadomf  8697  konigthlem  8720  axrepndlem2  8745  axunnd  8748  axpowndlem2  8750  axpowndlem2OLD  8751  axpowndlem4  8754  axregndlem2  8757  axacndlem5  8765  zfcndrep  8768  zfcndpow  8770  zfcndinf  8772  zfcndac  8773  pwfseqlem4a  8815  pwfseqlem4  8816  tskuni  8937  gruiin  8964  grothprim  8988  reclem2pr  9204  dedekind  9520  dedekindle  9521  fimaxre3  10266  uzindOLD  10723  nn0ind-raph  10729  uzind4s  10901  nnwof  10908  lbzbi  10930  fzrevral  11527  seqof2  11847  rlim2  12957  ello1mpt  12982  climeu  13016  o1compt  13048  summolem2a  13175  zsum  13178  sumss  13184  sumss2  13186  fsumcvg2  13187  fsum2dlem  13220  fsum00  13243  o1fsum  13258  prmind2  13756  iserodd  13884  pcmpt  13936  pcmptdvds  13938  mreexexd  14568  catpropd  14630  invfuc  14866  natpropd  14868  fucpropd  14869  acsmapd  15330  gsum2d2lem  16438  gsumcom2  16440  dprdwd  16468  dprdwdOLD  16474  dprd2d2  16516  mdetralt2  18256  mdetunilem2  18260  madugsum  18290  gsummatr01lem4  18305  neiptopnei  18577  neiptopreu  18578  neitr  18625  fiuncmp  18848  bwthOLD  18855  iunconlem  18872  iuncon  18873  2ndcdisj  18901  elptr2  18988  ptbasfi  18995  ptcld  19027  ptcldmpt  19028  ptclsg  19029  ptcnplem  19035  ptcnp  19036  cnmpt11  19077  cnmpt21  19085  cnmptcom  19092  imasnopn  19104  imasncld  19105  imasncls  19106  xkocnv  19228  elmptrab  19241  isfildlem  19271  alexsubALTlem3  19462  cnextfvval  19478  utopsnneiplem  19663  isucn2  19695  cfilucfilOLD  19985  cfilucfil  19986  blval2  19991  restmetu  20003  ovoliunlem3  20828  ovoliun  20829  ovoliun2  20830  ovoliunnul  20831  finiunmbl  20866  volfiniun  20869  iundisj  20870  iunmbl  20875  voliun  20876  iunmbl2  20879  mbfeqalem  20961  mbfsup  20983  mbfinf  20984  mbflim  20987  itg2splitlem  21067  itg2split  21068  isibl2  21085  cbvitg  21094  itgeqa  21132  itgss3  21133  itgfsum  21145  itgabs  21153  itggt0  21160  itgcn  21161  limcmpt  21199  limciun  21210  dvmptfsum  21288  dvlipcn  21307  dvfsumlem2  21340  dvfsumlem4  21342  dvfsumrlim  21344  dvfsum2  21347  itgsubst  21362  coeeq2  21594  dgrle  21595  ulmss  21746  leibpi  22221  rlimcnp  22243  rlimcnp2  22244  o1cxp  22252  fsumdvdscom  22409  lgseisenlem2  22573  dchrisumlema  22621  dchrisumlem2  22623  dchrisumlem3  22624  tgldim0eq  22837  colline  22917  f1otrg  22939  mptelee  22963  ex-natded9.26  23448  isch3  24466  atom1d  25579  chirred  25621  spc2ed  25679  19.9d2r  25685  clelsb3f  25686  mo5f  25691  rmoeq  25694  rmo4fOLD  25703  rmo4f  25704  elabreximdv  25715  rabss3d  25718  iuninc  25734  cbvdisjf  25740  disjorf  25746  disjabrex  25749  iundisjf  25754  disjunsn  25759  dfrel4  25760  ssrelf  25768  dfimafnf  25773  suppss2f  25777  cbvmptf  25794  feqmptdf  25801  fmptcof2  25802  ofpreima  25807  funcnvmptOLD  25809  funcnv5mpt  25811  funcnv4mpt  25812  cnvoprab  25846  f1od2  25847  fcobijfs  25849  fpwrelmapffslem  25856  fpwrelmap  25857  xrofsup  25877  iundisjfi  25902  nnindf  25911  nn0min  25912  isarchi3  26027  gsummptf1o  26098  isarchiofld  26137  ordtconlem1  26207  qqhval2  26264  esumeq12dva  26341  esumeq2dv  26347  esumc  26358  esumadd  26360  gsumesum  26363  esumlub  26364  esumpr  26369  esumfzf  26371  esumfsup  26372  esumpcvgval  26380  esumpmono  26381  esumcocn  26382  hasheuni  26387  esumcvg  26388  measvunilem  26479  measvunilem0  26480  measvuni  26481  measiuns  26484  measiun  26485  measinblem  26487  voliune  26498  volfiniune  26499  volmeas  26500  ddemeas  26505  eulerpartlemgvv  26606  dstrvprob  26701  ballotlemodife  26727  lgamgulmlem2  26863  lgamgulmlem6  26867  cvmcov  26999  untsucf  27207  nfcprod1  27269  nfcprod  27270  prodmolem2a  27293  zprod  27296  fprod  27300  fprodntriv  27301  prodss  27306  fprodn0  27336  fprod2dlem  27337  mpteq12d  27429  setinds2  27439  dfon2lem1  27442  dfon2lem3  27444  wfisg  27516  wfis2g  27520  trpredmintr  27541  frinsg  27552  frins2g  27556  frins2  27557  nfwrecs  27565  wfr3g  27569  frr3g  27613  wl-equsb3  28226  wl-mo2d  28238  wl-sb8eut  28239  ptrest  28266  heicant  28267  mbfposadd  28280  itgabsnc  28302  itggt0cn  28305  ftc1anclem5  28312  finminlem  28354  upixp  28464  indexa  28468  indexdom  28469  filbcmb  28475  sdclem2  28479  sdclem1  28480  fdc1  28483  totbndbnd  28529  sbcalf  28761  sbcexf  28762  scottexf  28822  scott0f  28823  prtlem5  28843  mzpexpmpt  28923  eq0rabdioph  28957  rexrabdioph  28974  rexfrabdioph  28975  elnn0rabdioph  28983  dvdsrabdioph  28990  fphpd  28997  monotuz  29124  monotoddzz  29126  oddcomabszz  29127  setindtr  29215  dford4  29220  wdom2d2  29226  aomclem6  29254  aomclem8  29256  flcidc  29373  areaquad  29434  pm10.12  29452  19.31vv  29478  aaanv  29483  pm11.57  29484  pm11.58  29485  pm11.59  29486  pm11.71  29492  axc11next  29502  pm13.192  29506  pm14.12  29517  evth2f  29579  elunif  29580  fvelrnbf  29582  evthf  29591  fnchoice  29593  sumpair  29599  rfcnnnub  29600  refsum2cn  29602  fmul01  29603  fmuldfeqlem1  29605  fmuldfeq  29606  fmul01lt1lem1  29607  fmul01lt1lem2  29608  fmul01lt1  29609  infrglb  29614  climexp  29621  climsuse  29624  climrecf  29625  climinff  29627  stoweidlem3  29641  stoweidlem14  29652  stoweidlem17  29655  stoweidlem19  29657  stoweidlem20  29658  stoweidlem26  29664  stoweidlem27  29665  stoweidlem28  29666  stoweidlem29  29667  stoweidlem31  29669  stoweidlem34  29672  stoweidlem35  29673  stoweidlem36  29674  stoweidlem39  29677  stoweidlem42  29680  stoweidlem43  29681  stoweidlem44  29682  stoweidlem46  29684  stoweidlem48  29686  stoweidlem49  29687  stoweidlem50  29688  stoweidlem51  29689  stoweidlem52  29690  stoweidlem53  29691  stoweidlem54  29692  stoweidlem56  29694  stoweidlem57  29695  stoweidlem59  29697  stoweidlem60  29698  stoweidlem61  29699  stoweidlem62  29700  stoweid  29701  wallispilem3  29705  stirlinglem13  29724  stirling  29727  rexsb  29835  rmoanim  29846  2reu4a  29856  ffnafv  29920  oprabv  30000  rabasiun  30073  opeliun2xp  30562  cbvmpt2x2  30567  ovmpt2rdx  30571  ssralv2  30934  tratrb  30940  iunconlem2  31370  bnj919  31459  bnj1146  31484  bnj1379  31523  bnj1385  31525  bnj1400  31528  bnj1476  31539  bnj1534  31545  bnj1542  31549  bnj110  31550  bnj121  31562  bnj124  31563  bnj130  31566  bnj207  31573  bnj571  31598  bnj605  31599  bnj580  31605  bnj607  31608  bnj611  31610  bnj873  31616  bnj849  31617  bnj900  31621  bnj916  31625  bnj1000  31633  bnj964  31635  bnj981  31642  bnj985  31645  bnj1014  31652  bnj1123  31676  bnj1128  31680  bnj1228  31701  bnj1204  31702  bnj1279  31708  bnj1307  31713  bnj1321  31717  bnj1388  31723  bnj1398  31724  bnj1408  31726  bnj1417  31731  bnj1444  31733  bnj1445  31734  bnj1446  31735  bnj1449  31738  bnj1467  31744  bnj1489  31746  bnj1312  31748  bnj1497  31750  bnj1518  31754  bnj1525  31759  bnj1529  31760  bj-spimvv  31846  bj-spimevv  31847  bj-chvarvv  31851  bj-cbv3v2  31853  bj-cbvalvv  31862  bj-cbvexvv  31863  bj-cbvaldv  31864  bj-cbval2v  31866  bj-cbval2vv  31868  bj-cbvex2vv  31869  bj-cbvaldvav  31870  bj-cbvexdvav  31871  bj-drnf2v  31892  bj-abbi  31915  bj-abbidv  31919  bj-axrep1  31926  bj-axrep2  31927  bj-axrep3  31928  bj-axrep4  31929  bj-axrep5  31930  bj-axsep  31931  ax11-pm2  31961  bj-clelsb3  31968  bj-nfcjust  31970  bj-inrab2  32014  riotasv2d  32178  riotasv2s  32179  riotasv3d  32181  glbconxN  32592  pmapglbx  32983  pmapglb2xN  32986  cdleme26ee  33574  cdleme31sn  33594  cdleme31sn1  33595  cdlemefr29exN  33616  cdlemefs32sn1aw  33628  cdleme43fsv1snlem  33634  cdleme41sn3a  33647  cdleme32fva  33651  cdleme32d  33658  cdleme32f  33660  cdleme40m  33681  cdleme40n  33682  cdleme42b  33692  cdlemk36  34127  cdlemk38  34129  cdlemkid  34150  cdlemk19x  34157  cdlemk11t  34160  dihvalcqpre  34450  mapdheq  34943  hdmap1eq  35017  hdmapval2lem  35049
  Copyright terms: Public domain W3C validator