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

Theorem nfv 1673
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 1670 . 2  |-  ( ph  ->  A. x ph )
21nfi 1596 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-5 1670
This theorem depends on definitions:  df-bi 185  df-nf 1590
This theorem is referenced by:  nfvd  1674  nexdv  1818  dvelimhw  1881  19.21v  1909  19.23v  1910  pm11.53  1912  19.27v  1913  19.28v  1914  19.36v  1915  19.36aiv  1916  19.12vv  1917  19.37v  1918  19.41v  1920  19.42v  1924  eeanv  1932  eeeanv  1933  spimv  1953  spimev  1954  chvarv  1958  cbvalv  1971  cbvexv  1972  cbvald  1973  cbval2  1975  cbvex2OLD  1977  cbval2v  1978  cbvex2v  1979  cbvaldva  1980  cbvexdva  1981  axc9lem2  1988  axc16i  2012  dvelimnf  2031  cleljustALT  2060  sbiedv  2104  equsb3lem  2136  equsb3  2137  equsb3ALT  2138  elsb3  2139  elsb4  2140  sbhb  2143  sbnf2  2144  sbnf2OLD  2145  sbcom2  2151  sbcom4  2153  dfsb7  2165  sbid2v  2167  sbel2x  2169  sbco4lem  2178  sbco4  2179  exsb  2180  2exsb  2181  euf  2261  eufOLD  2262  mo2  2263  nfeud2  2266  eubidv  2274  mobidv  2275  nfeud2OLD  2278  sb8eu  2290  sb8euOLD  2291  sb8euOLDOLD  2292  mo3OLD  2297  moOLD  2303  euexALT  2304  eu5OLD  2307  euorv  2309  sbmo  2313  mo4f  2314  mo4  2315  morimvOLD  2320  moanimOLD  2331  moanimv  2332  euanv  2336  mopickOLD  2338  mopickOLDOLD  2339  moexexv  2349  2mo  2357  2moOLD  2358  2moOLDOLD  2359  2mos  2360  2eu4OLD  2365  2eu6  2367  2eu6OLD  2368  bm1.1  2423  eqsb3lem  2538  eqsb3  2539  clelsb3  2540  abbi  2548  abbidv  2552  cbvabv  2557  clelab  2558  nfcjust  2562  nfcv  2574  nfeqd  2588  nfeld  2589  nfabd2  2592  dvelimdc  2594  cleqf  2598  sbabel  2600  ralbidva  2726  rexbidva  2727  ralbidv  2730  rexbidv  2731  2ralbida  2749  2ralbidva  2750  ralimdva  2789  ralrimiv  2793  r19.21v  2798  ralrimdv  2800  reximdvai  2821  r19.23v  2828  rexlimiv  2830  rexlimdv  2835  r19.29af  2856  r19.29a  2857  r19.37av  2865  r19.41v  2868  reean  2882  reeanv  2883  reubidva  2899  rmobidva  2904  cbvralf  2936  cbvreu  2940  cbvralv  2942  cbvrexv  2943  cbvreuv  2944  cbvrmov  2945  cbvralsv  2953  cbvrexsv  2954  sbralie  2955  cbvrab  2965  cbvrabv  2966  issetf  2972  ceqsalv  2995  ceqsralv  2996  ceqsexv  3004  ceqsex2  3005  ceqsex2v  3006  vtocld  3017  vtocl  3019  vtoclg  3025  vtocl2g  3029  vtoclga  3031  vtocl2gaf  3032  vtocl2ga  3033  vtocl3gaf  3034  vtocl3ga  3035  spcimdv  3049  spcgv  3052  spcegv  3053  rspct  3061  rspc  3062  rspce  3063  rspcv  3064  rspcev  3068  rspc2v  3074  eqvincf  3082  ceqsexgv  3087  elabgt  3098  elab  3101  elabg  3102  elab3g  3107  elrab3t  3111  elrab  3112  ralab2  3119  rexab2  3121  mob2  3134  mob  3136  reu2  3142  nfcdeq  3178  sbcco  3204  sbcco2  3205  cbvsbcv  3211  sbcieg  3214  sbcie2g  3215  sbcied  3218  elrabsf  3220  sbcbidv  3240  sbcg  3255  sbc2iegf  3256  sbc2ie  3257  rmo2  3278  rmo3  3280  nfcsb1d  3297  nfcsbd  3300  csbiebt  3303  csbied  3309  csbie2t  3311  cbvralcsf  3314  cbvreucsf  3316  cbvrabcsf  3317  cbvralv2  3318  cbvrexv2  3319  dfss2f  3342  uniiunlem  3435  rspn0  3644  csbeq2dv  3682  sbcnestg  3688  sbnfc2  3701  sbss  3784  nfifd  3812  rabsnifsb  3938  euabsn  3942  nfuni  4092  nfunid  4093  eluniab  4097  nfint  4133  elintab  4134  iineq2dv  4188  disjiun  4277  disjxun  4285  opabbidv  4350  nfopab  4352  cbvopab  4355  cbvopabv  4356  cbvopab1  4357  cbvopab2  4358  cbvopab1s  4359  cbvopab1v  4360  mpteq12f  4363  mpteq2dva  4373  cbvmpt  4377  axrep1  4399  axrep2  4400  axrep3  4401  axrep4  4402  axrep5  4403  zfrepclf  4404  axsep  4407  zfnuleu  4413  reusv2lem2  4489  reusv2lem3  4490  reusv2lem4  4491  reusv2  4493  reusv3  4495  reusv6OLD  4498  alxfr  4500  ralxfrALT  4506  copsex2t  4573  copsex2g  4574  opelopabaf  4607  nfso  4642  pofun  4652  nffr  4689  opeliunxp  4885  opeliunxp2  4973  ralxpf  4981  dfdmf  5028  dfrnf  5073  elrnmpt1  5083  asymref2  5210  intirr  5211  nfiotad  5379  cbviota  5381  cbviotav  5382  sb8iota  5383  iota2d  5401  iota2  5402  dffun6f  5427  fun11  5478  imadif  5488  funimaexg  5490  isarep1  5492  isarep2  5493  fv3  5698  tz6.12f  5703  tz6.12c  5704  opabiotafun  5747  funfv2f  5755  fvmptdf  5780  fvmptdv  5781  fvmptt  5784  fvopab5  5790  eqfnfv2f  5796  ralrnmpt  5847  f1ompt  5860  ffnfv  5864  ffnfvf  5865  fmptco  5871  elabrex  5955  dff13f  5968  fliftfun  6000  cbvriota  6057  cbvriotav  6058  riota2  6070  riota5f  6072  nfoprab  6133  oprabbidv  6135  mpt2eq123  6140  cbvoprab1  6153  cbvoprab2  6154  cbvoprab12  6155  cbvoprab12v  6156  cbvoprab3  6157  cbvoprab3v  6158  cbvmpt2x  6159  ralrnmpt2  6200  ovmpt2dx  6212  ovmpt2df  6217  ovmpt2dv  6218  ov3  6222  ofrfval2  6332  onminex  6413  tfis  6460  tfis2  6462  tfisi  6464  tfinds  6465  tfindes  6468  peano5  6494  findes  6501  fun11iun  6532  abrexex2g  6549  opabex3d  6550  opabex3  6551  abrexex2  6553  dfoprab4f  6627  fmpt2x  6635  offval22  6647  ovmptss  6649  tposoprab  6776  nfrecs  6826  tfr3  6850  nfrdg  6862  tz7.48-1  6890  tz7.49  6892  eqerlem  7125  erovlem  7188  mptelixpg  7292  boxcutc  7298  dom2lem  7341  xpf1o  7465  mapxpen  7469  nneneq  7486  pssnn  7523  findcard2  7544  ac6sfi  7548  fiint  7580  indexfi  7611  wdom2d  7787  ixpiunwdom  7798  sucprcregOLD  7807  cantnflem1  7889  r1val1  7985  rankuni2b  8052  scottexs  8086  scott0s  8087  dfac8clem  8194  acni2  8208  aceq1  8279  dfac5lem5  8289  kmlem15  8325  infpssrlem4  8467  fin23lem27  8489  hsmexlem2  8588  hsmexlem4  8590  axcc3  8599  domtriomlem  8603  axdc3lem2  8612  axdc3lem4  8614  axdc4lem  8616  ac6num  8640  ac6c4  8642  zorn2lem4  8660  zorn2lem5  8661  iunfo  8695  iundom2g  8696  uniimadomf  8701  konigthlem  8724  axrepndlem2  8749  axunnd  8752  axpowndlem2  8754  axpowndlem2OLD  8755  axpowndlem4  8758  axregndlem2  8761  axacndlem5  8770  zfcndrep  8773  zfcndpow  8775  zfcndinf  8777  zfcndac  8778  pwfseqlem4a  8820  pwfseqlem4  8821  tskuni  8942  gruiin  8969  grothprim  8993  reclem2pr  9209  dedekind  9525  dedekindle  9526  fimaxre3  10271  uzindOLD  10728  nn0ind-raph  10734  uzind4s  10906  nnwof  10913  lbzbi  10935  fzrevral  11536  seqof2  11856  rlim2  12966  ello1mpt  12991  climeu  13025  o1compt  13057  summolem2a  13184  zsum  13187  sumss  13193  sumss2  13195  fsumcvg2  13196  fsum2dlem  13229  fsum00  13253  o1fsum  13268  prmind2  13766  iserodd  13894  pcmpt  13946  pcmptdvds  13948  mreexexd  14578  catpropd  14640  invfuc  14876  natpropd  14878  fucpropd  14879  acsmapd  15340  gsummptshft  16419  gsummpt1n0  16446  gsum2d2lem  16455  gsumcom2  16457  dprdwd  16485  dprdwdOLD  16491  dprd2d2  16533  mdetralt2  18395  mdetunilem2  18399  madugsum  18429  gsummatr01lem4  18444  neiptopnei  18716  neiptopreu  18717  neitr  18764  fiuncmp  18987  bwthOLD  18994  iunconlem  19011  iuncon  19012  2ndcdisj  19040  elptr2  19127  ptbasfi  19134  ptcld  19166  ptcldmpt  19167  ptclsg  19168  ptcnplem  19174  ptcnp  19175  cnmpt11  19216  cnmpt21  19224  cnmptcom  19231  imasnopn  19243  imasncld  19244  imasncls  19245  xkocnv  19367  elmptrab  19380  isfildlem  19410  alexsubALTlem3  19601  cnextfvval  19617  utopsnneiplem  19802  isucn2  19834  cfilucfilOLD  20124  cfilucfil  20125  blval2  20130  restmetu  20142  ovoliunlem3  20967  ovoliun  20968  ovoliun2  20969  ovoliunnul  20970  finiunmbl  21005  volfiniun  21008  iundisj  21009  iunmbl  21014  voliun  21015  iunmbl2  21018  mbfeqalem  21100  mbfsup  21122  mbfinf  21123  mbflim  21126  itg2splitlem  21206  itg2split  21207  isibl2  21224  cbvitg  21233  itgeqa  21271  itgss3  21272  itgfsum  21284  itgabs  21292  itggt0  21299  itgcn  21300  limcmpt  21338  limciun  21349  dvmptfsum  21427  dvlipcn  21446  dvfsumlem2  21479  dvfsumlem4  21481  dvfsumrlim  21483  dvfsum2  21486  itgsubst  21501  coeeq2  21690  dgrle  21691  ulmss  21842  leibpi  22317  rlimcnp  22339  rlimcnp2  22340  o1cxp  22348  fsumdvdscom  22505  lgseisenlem2  22669  dchrisumlema  22717  dchrisumlem2  22719  dchrisumlem3  22720  tgldim0eq  22936  colline  23032  f1otrg  23085  mptelee  23109  ex-natded9.26  23594  isch3  24612  atom1d  25725  chirred  25767  spc2ed  25825  19.9d2r  25831  clelsb3f  25832  mo5f  25836  rmoeq  25839  rmo4fOLD  25848  rmo4f  25849  elabreximdv  25860  rabss3d  25863  iuninc  25879  cbvdisjf  25885  disjorf  25891  disjabrex  25894  iundisjf  25899  disjunsn  25904  dfrel4  25905  ssrelf  25913  dfimafnf  25918  suppss2f  25922  cbvmptf  25939  feqmptdf  25946  fmptcof2  25947  ofpreima  25952  funcnvmptOLD  25954  funcnv5mpt  25956  funcnv4mpt  25957  cnvoprab  25991  f1od2  25992  fcobijfs  25994  fpwrelmapffslem  26000  fpwrelmap  26001  xrofsup  26023  iundisjfi  26048  nnindf  26057  nn0min  26058  isarchi3  26172  gsummptf1o  26215  isarchiofld  26253  ordtconlem1  26323  qqhval2  26380  esumeq12dva  26457  esumeq2dv  26463  esumc  26474  esumadd  26476  gsumesum  26479  esumlub  26480  esumpr  26485  esumfzf  26487  esumfsup  26488  esumpcvgval  26496  esumpmono  26497  esumcocn  26498  hasheuni  26503  esumcvg  26504  measvunilem  26595  measvunilem0  26596  measvuni  26597  measiuns  26600  measiun  26601  measinblem  26603  voliune  26614  volfiniune  26615  volmeas  26616  ddemeas  26621  oms0  26679  eulerpartlemgvv  26728  eulerpart  26734  dstrvprob  26823  ballotlemodife  26849  lgamgulmlem2  26985  lgamgulmlem6  26989  cvmcov  27121  untsucf  27330  nfcprod1  27392  nfcprod  27393  prodmolem2a  27416  zprod  27419  fprod  27423  fprodntriv  27424  prodss  27429  fprodn0  27459  fprod2dlem  27460  mpteq12d  27552  setinds2  27562  dfon2lem1  27565  dfon2lem3  27567  wfisg  27639  wfis2g  27643  trpredmintr  27664  frinsg  27675  frins2g  27679  frins2  27680  nfwrecs  27688  wfr3g  27692  frr3g  27736  wl-equsb3  28349  wl-lem-mo-recur  28364  wl-lem-moreduce  28365  wl-sb8eut  28369  ptrest  28396  heicant  28397  mbfposadd  28410  itgabsnc  28432  itggt0cn  28435  ftc1anclem5  28442  finminlem  28484  upixp  28594  indexa  28598  indexdom  28599  filbcmb  28605  sdclem2  28609  sdclem1  28610  fdc1  28613  totbndbnd  28659  sbcalf  28891  sbcexf  28892  scottexf  28951  scott0f  28952  prtlem5  28972  mzpexpmpt  29052  eq0rabdioph  29086  rexrabdioph  29103  rexfrabdioph  29104  elnn0rabdioph  29112  dvdsrabdioph  29119  fphpd  29126  monotuz  29253  monotoddzz  29255  oddcomabszz  29256  setindtr  29344  dford4  29349  wdom2d2  29355  aomclem6  29383  aomclem8  29385  flcidc  29502  areaquad  29563  pm10.12  29581  19.31vv  29607  aaanv  29612  pm11.57  29613  pm11.58  29614  pm11.59  29615  pm11.71  29621  axc11next  29631  pm13.192  29635  pm14.12  29646  evth2f  29708  elunif  29709  fvelrnbf  29711  evthf  29720  fnchoice  29722  sumpair  29728  rfcnnnub  29729  refsum2cn  29731  fmul01  29732  fmuldfeqlem1  29734  fmuldfeq  29735  fmul01lt1lem1  29736  fmul01lt1lem2  29737  fmul01lt1  29738  infrglb  29742  climexp  29749  climsuse  29752  climrecf  29753  climinff  29755  stoweidlem3  29769  stoweidlem14  29780  stoweidlem17  29783  stoweidlem19  29785  stoweidlem20  29786  stoweidlem26  29792  stoweidlem27  29793  stoweidlem28  29794  stoweidlem29  29795  stoweidlem31  29797  stoweidlem34  29800  stoweidlem35  29801  stoweidlem36  29802  stoweidlem39  29805  stoweidlem42  29808  stoweidlem43  29809  stoweidlem44  29810  stoweidlem46  29812  stoweidlem48  29814  stoweidlem49  29815  stoweidlem50  29816  stoweidlem51  29817  stoweidlem52  29818  stoweidlem53  29819  stoweidlem54  29820  stoweidlem56  29822  stoweidlem57  29823  stoweidlem59  29825  stoweidlem60  29826  stoweidlem61  29827  stoweidlem62  29828  stoweid  29829  wallispilem3  29833  stirlinglem13  29852  stirling  29855  rexsb  29963  rmoanim  29974  2reu4a  29984  ffnafv  30048  oprabv  30128  rabasiun  30201  opeliun2xp  30690  cbvmpt2x2  30696  ovmpt2rdx  30700  rabssnn0fi  30716  fsuppmapnn0fiublem  30767  fsuppmapnn0fiub  30768  fsuppmapnn0fiubex  30769  gsummptnn0fz  30775  gsummptnn0fzv  30776  gsummoncoe1  30808  ssralv2  31165  tratrb  31171  iunconlem2  31600  bnj919  31689  bnj1146  31714  bnj1379  31753  bnj1385  31755  bnj1400  31758  bnj1476  31769  bnj1534  31775  bnj1542  31779  bnj110  31780  bnj121  31792  bnj124  31793  bnj130  31796  bnj207  31803  bnj571  31828  bnj605  31829  bnj580  31835  bnj607  31838  bnj611  31840  bnj873  31846  bnj849  31847  bnj900  31851  bnj916  31855  bnj1000  31863  bnj964  31865  bnj981  31872  bnj985  31875  bnj1014  31882  bnj1123  31906  bnj1128  31910  bnj1228  31931  bnj1204  31932  bnj1279  31938  bnj1307  31943  bnj1321  31947  bnj1388  31953  bnj1398  31954  bnj1408  31956  bnj1417  31961  bnj1444  31963  bnj1445  31964  bnj1446  31965  bnj1449  31968  bnj1467  31974  bnj1489  31976  bnj1312  31978  bnj1497  31980  bnj1518  31984  bnj1525  31989  bnj1529  31990  bj-spimvv  32119  bj-spimevv  32120  bj-chvarvv  32124  bj-cbv3v2  32126  bj-cbvalvv  32135  bj-cbvexvv  32136  bj-cbvaldv  32137  bj-cbval2v  32139  bj-cbval2vv  32141  bj-cbvex2vv  32142  bj-cbvaldvav  32143  bj-cbvexdvav  32144  bj-drnf2v  32165  bj-abbi  32197  bj-abbidv  32201  bj-axrep1  32210  bj-axrep2  32211  bj-axrep3  32212  bj-axrep4  32213  bj-axrep5  32214  bj-axsep  32215  ax11-pm2  32245  bj-clelsb3  32259  bj-nfcjust  32261  bj-ceqsalv  32294  bj-vtocl  32316  bj-inrab2  32331  riotasv2d  32501  riotasv2s  32502  riotasv3d  32504  glbconxN  32915  pmapglbx  33306  pmapglb2xN  33309  cdleme26ee  33897  cdleme31sn  33917  cdleme31sn1  33918  cdlemefr29exN  33939  cdlemefs32sn1aw  33951  cdleme43fsv1snlem  33957  cdleme41sn3a  33970  cdleme32fva  33974  cdleme32d  33981  cdleme32f  33983  cdleme40m  34004  cdleme40n  34005  cdleme42b  34015  cdlemk36  34450  cdlemk38  34452  cdlemkid  34473  cdlemk19x  34480  cdlemk11t  34483  dihvalcqpre  34773  mapdheq  35266  hdmap1eq  35340  hdmapval2lem  35372
  Copyright terms: Public domain W3C validator