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

Theorem nfv 1683
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 1680 . 2  |-  ( ph  ->  A. x ph )
21nfi 1606 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-nf 1600
This theorem is referenced by:  nfvd  1684  nexdv  1832  dvelimhw  1902  19.21vOLD  1931  19.23vOLD  1933  pm11.53  1937  19.27v  1938  19.28v  1939  19.36vOLD  1940  19.36aivOLD  1941  19.12vv  1942  19.37v  1943  19.41v  1945  19.42v  1949  eeanv  1957  eeeanv  1958  spimv  1978  spimev  1979  chvarv  1983  cbvalv  1996  cbvexv  1997  cbvald  1998  cbval2  2000  cbvex2OLD  2002  cbval2v  2003  cbvex2v  2004  cbvaldva  2005  cbvexdva  2006  axc9lem2  2013  axc16i  2037  dvelimnf  2054  cleljustALT  2083  sbiedv  2127  equsb3lem  2158  equsb3  2159  equsb3ALT  2160  elsb3  2161  elsb4  2162  sbhb  2165  sbnf2  2166  sbnf2OLD  2167  sbcom2  2173  sbcom4  2175  dfsb7  2187  sbid2v  2189  sbel2x  2191  sbco4lem  2200  sbco4  2201  2sb8e  2202  exsb  2203  euf  2285  eufOLD  2286  mo2  2287  nfeud2  2290  eubidv  2298  mobidv  2299  nfeud2OLD  2302  sb8eu  2314  sb8euOLD  2315  sb8euOLDOLD  2316  mo3OLD  2321  moOLD  2327  euexALT  2328  eu5OLD  2331  euorv  2333  sbmo  2337  mo4f  2338  mo4  2339  morimvOLD  2344  moanimOLD  2355  moanimv  2356  euanv  2360  mopickOLD  2362  mopickOLDOLD  2363  moexexv  2373  2mo  2382  2moOLD  2383  2moOLDOLD  2384  2mos  2385  2eu4OLD  2391  2eu6  2393  2eu6OLD  2394  bm1.1  2450  bm1.1OLD  2451  cleqh  2582  eqsb3lem  2586  eqsb3  2587  clelsb3  2588  abbiOLD  2599  abbidv  2603  cbvabv  2610  clelab  2611  clelabOLD  2612  nfcjust  2616  nfcv  2629  nfeqd  2636  nfeld  2637  nfabd2  2650  dvelimdc  2652  cleqfOLD  2657  sbabel  2660  sbabelOLD  2661  r19.21vOLD  2870  ralimdvaOLD  2873  ralrimivOLD  2877  ralrimdvOLD  2881  ralbidvaOLD  2901  ralbidvOLD  2904  2ralbida  2905  2ralbidvaOLD  2907  reximdvaiOLD  2936  r19.23vOLD  2944  rexlimivOLD  2950  rexlimdvOLD  2954  rexbidvaALT  2971  rexbidvALT  2974  r19.29af  3001  r19.29an  3002  r19.29a  3003  r19.37av  3011  r19.41v  3014  reean  3028  reeanv  3029  reubidva  3045  rmobidva  3050  cbvralf  3082  cbvreu  3086  cbvralv  3088  cbvrexv  3089  cbvreuv  3090  cbvrmov  3091  cbvralsv  3099  cbvrexsv  3100  sbralie  3101  cbvrab  3111  cbvrabv  3112  issetf  3118  ceqsalv  3141  ceqsralv  3142  ceqsexv  3150  ceqsex2  3151  ceqsex2v  3152  vtocld  3163  vtocl  3165  vtoclg  3171  vtocl2g  3175  vtoclga  3177  vtocl2gaf  3178  vtocl2ga  3179  vtocl3gaf  3180  vtocl3ga  3181  spcimdv  3195  spcgv  3198  spcegv  3199  rspct  3207  rspc  3208  rspce  3209  rspcv  3210  rspcev  3214  rspc2v  3223  eqvincf  3231  ceqsexgv  3236  elabgt  3247  elab  3250  elabg  3251  elab3g  3256  elrab3t  3260  elrab  3261  ralab2  3268  rexab2  3270  mob2  3283  mob  3285  reu2  3291  reu2eqd  3300  nfcdeq  3328  sbcco  3354  sbcco2  3355  cbvsbcv  3361  sbcieg  3364  sbcie2g  3365  sbcied  3368  elrabsf  3370  sbcbidv  3390  sbcg  3405  sbc2iegf  3406  sbc2ie  3407  rmo2  3428  rmo3  3430  nfcsb1d  3449  nfcsbd  3452  csbiebt  3455  csbied  3462  csbie2t  3464  cbvralcsf  3467  cbvreucsf  3469  cbvrabcsf  3470  cbvralv2  3471  cbvrexv2  3472  dfss2f  3495  uniiunlem  3588  rspn0  3797  csbeq2dv  3835  sbcnestg  3841  sbnfc2  3854  sbss  3937  nfifd  3967  rabsnifsb  4095  euabsn  4099  nfuni  4251  nfunid  4252  eluniab  4256  nfint  4292  elintab  4293  rabasiun  4329  iineq2dv  4348  disjiun  4437  disjxun  4445  opabbidv  4510  nfopab  4512  cbvopab  4515  cbvopabv  4516  cbvopab1  4517  cbvopab2  4518  cbvopab1s  4519  cbvopab1v  4520  mpteq12f  4523  mpteq2dva  4533  cbvmpt  4537  axrep1  4559  axrep2  4560  axrep3  4561  axrep4  4562  axrep5  4563  zfrepclf  4564  axsep  4567  zfnuleu  4573  reusv2lem2  4649  reusv2lem3  4650  reusv2lem4  4651  reusv2  4653  reusv3  4655  reusv6OLD  4658  alxfr  4660  ralxfrALT  4666  copsex2t  4734  copsex2g  4735  opelopabaf  4771  nfso  4806  pofun  4816  nffr  4853  opeliunxp  5050  opeliunxp2  5139  ralxpf  5147  dfdmf  5194  dfrnf  5239  elrnmpt1  5249  asymref2  5382  intirr  5383  nfiotad  5552  cbviota  5554  cbviotav  5555  sb8iota  5556  iota2d  5574  iota2  5575  dffun6f  5600  fun11  5651  imadif  5661  funimaexg  5663  isarep1  5665  isarep2  5666  fv3  5877  tz6.12f  5882  tz6.12c  5883  opabiotafun  5926  funfv2f  5934  fvmptdf  5959  fvmptdv  5960  fvmptt  5963  fvopab5  5971  eqfnfv2f  5977  ralrnmpt  6028  f1ompt  6041  ffnfv  6045  ffnfvf  6046  fmptco  6052  elabrex  6141  dff13f  6153  fliftfun  6196  cbvriota  6253  cbvriotav  6254  riota2  6266  riota5f  6268  oprabv  6327  nfoprab  6331  oprabbidv  6333  mpt2eq123  6338  cbvoprab1  6351  cbvoprab2  6352  cbvoprab12  6353  cbvoprab12v  6354  cbvoprab3  6355  cbvoprab3v  6356  cbvmpt2x  6357  ralrnmpt2  6399  ovmpt2dx  6411  ovmpt2df  6416  ovmpt2dv  6417  ov3  6421  ofrfval2  6539  onminex  6620  tfis  6667  tfis2  6669  tfisi  6671  tfinds  6672  tfindes  6675  peano5  6701  findes  6708  fun11iun  6741  abrexex2g  6758  opabex3d  6759  opabex3  6760  abrexex2  6762  dfoprab4f  6839  fmpt2x  6847  offval22  6859  ovmptss  6861  tposoprab  6988  fvmpt2curryd  6997  nfrecs  7041  tfr3  7065  nfrdg  7077  tz7.48-1  7105  tz7.49  7107  eqerlem  7340  erovlem  7404  mptelixpg  7503  boxcutc  7509  dom2lem  7552  xpf1o  7676  mapxpen  7680  nneneq  7697  pssnn  7735  findcard2  7756  ac6sfi  7760  fiint  7793  indexfi  7824  wdom2d  8002  ixpiunwdom  8013  sucprcregOLD  8022  cantnflem1  8104  r1val1  8200  rankuni2b  8267  scottexs  8301  scott0s  8302  dfac8clem  8409  acni2  8423  aceq1  8494  dfac5lem5  8504  kmlem15  8540  infpssrlem4  8682  fin23lem27  8704  hsmexlem2  8803  hsmexlem4  8805  axcc3  8814  domtriomlem  8818  axdc3lem2  8827  axdc3lem4  8829  axdc4lem  8831  ac6num  8855  ac6c4  8857  zorn2lem4  8875  zorn2lem5  8876  iunfo  8910  iundom2g  8911  uniimadomf  8916  konigthlem  8939  axrepndlem2  8964  axunnd  8967  axpowndlem2  8969  axpowndlem2OLD  8970  axpowndlem4  8973  axregndlem2  8976  axacndlem5  8985  zfcndrep  8988  zfcndpow  8990  zfcndinf  8992  zfcndac  8993  pwfseqlem4a  9035  pwfseqlem4  9036  tskuni  9157  gruiin  9184  grothprim  9208  reclem2pr  9422  dedekind  9739  dedekindle  9740  fimaxre3  10488  uzindOLD  10951  nn0ind-raph  10957  uzind4s  11137  nnwof  11144  lbzbi  11166  fzrevral  11758  rabssnn0fi  12059  fsuppmapnn0fiublem  12060  fsuppmapnn0fiub  12061  fsuppmapnn0fiubex  12062  seqof2  12129  rlim2  13278  ello1mpt  13303  climeu  13337  o1compt  13369  summolem2a  13496  zsum  13499  sumss  13505  sumss2  13507  fsumcvg2  13508  fsum2dlem  13544  fsum00  13571  o1fsum  13586  prmind2  14083  iserodd  14214  pcmpt  14266  pcmptdvds  14268  mreexexd  14899  catpropd  14961  invfuc  15197  natpropd  15199  fucpropd  15200  acsmapd  15661  gsummptshft  16747  gsumsnd  16770  gsumsnf  16771  gsumunsnfd  16774  gsummptf1o  16781  gsummpt1n0  16783  gsum2d2lem  16792  gsumcom2  16794  gsummptnn0fz  16805  gsummptnn0fzv  16806  dprdwd  16835  dprdwdOLD  16841  dprd2d2  16883  gsummoncoe1  18117  gsumply1eq  18118  mdetralt2  18878  mdetunilem2  18882  madugsum  18912  gsummatr01lem4  18927  cpmatmcllem  18986  pmatcollpwfi  19050  cayleyhamilton1  19160  neiptopnei  19399  neiptopreu  19400  neitr  19447  fiuncmp  19670  bwthOLD  19677  iunconlem  19694  iuncon  19695  2ndcdisj  19723  elptr2  19810  ptbasfi  19817  ptcld  19849  ptcldmpt  19850  ptclsg  19851  ptcnplem  19857  ptcnp  19858  cnmpt11  19899  cnmpt21  19907  cnmptcom  19914  imasnopn  19926  imasncld  19927  imasncls  19928  xkocnv  20050  elmptrab  20063  isfildlem  20093  alexsubALTlem3  20284  cnextfvval  20300  utopsnneiplem  20485  isucn2  20517  cfilucfilOLD  20807  cfilucfil  20808  blval2  20813  restmetu  20825  ovoliunlem3  21650  ovoliun  21651  ovoliun2  21652  ovoliunnul  21653  finiunmbl  21689  volfiniun  21692  iundisj  21693  iunmbl  21698  voliun  21699  iunmbl2  21702  mbfeqalem  21784  mbfsup  21806  mbfinf  21807  mbflim  21810  itg2splitlem  21890  itg2split  21891  isibl2  21908  cbvitg  21917  itgeqa  21955  itgss3  21956  itgfsum  21968  itgabs  21976  itggt0  21983  itgcn  21984  limcmpt  22022  limciun  22033  dvmptfsum  22111  dvlipcn  22130  dvfsumlem2  22163  dvfsumlem4  22165  dvfsumrlim  22167  dvfsum2  22170  itgsubst  22185  coeeq2  22374  dgrle  22375  ulmss  22526  leibpi  23001  rlimcnp  23023  rlimcnp2  23024  o1cxp  23032  fsumdvdscom  23189  lgseisenlem2  23353  dchrisumlema  23401  dchrisumlem2  23403  dchrisumlem3  23404  istrkg2ld  23586  tgldim0eq  23622  colline  23743  f1otrg  23850  mptelee  23874  ex-natded9.26  24817  isch3  25835  atom1d  26948  chirred  26990  spc2ed  27048  19.9d2r  27054  clelsb3f  27055  mo5f  27059  rmoeq  27062  rmo4fOLD  27071  rmo4f  27072  elabreximdv  27083  rabss3d  27086  iuninc  27101  cbvdisjf  27107  disjorf  27113  disjabrex  27116  iundisjf  27121  disjunsn  27126  dfrel4  27127  ssrelf  27139  dfimafnf  27146  suppss2f  27150  cbvmptf  27166  feqmptdf  27173  fmptcof2  27174  ofpreima  27179  funcnvmptOLD  27181  funcnv5mpt  27183  funcnv4mpt  27184  cnvoprab  27218  f1od2  27219  fcobijfs  27221  fpwrelmapffslem  27227  fpwrelmap  27228  xrofsup  27250  iundisjfi  27269  nnindf  27278  nn0min  27279  isarchi3  27393  isarchiofld  27470  ordtconlem1  27542  qqhval2  27599  esumeq12dva  27685  esumeq2dv  27691  esumc  27702  esumadd  27704  gsumesum  27707  esumlub  27708  esumpr  27713  esumfzf  27715  esumfsup  27716  esumpcvgval  27724  esumpmono  27725  esumcocn  27726  hasheuni  27731  esumcvg  27732  measvunilem  27823  measvunilem0  27824  measvuni  27825  measiuns  27828  measiun  27829  measinblem  27831  voliune  27841  volfiniune  27842  volmeas  27843  ddemeas  27848  oms0  27906  eulerpartlemgvv  27955  eulerpart  27961  dstrvprob  28050  ballotlemodife  28076  lgamgulmlem2  28212  lgamgulmlem6  28216  cvmcov  28348  untsucf  28557  nfcprod1  28619  nfcprod  28620  prodmolem2a  28643  zprod  28646  fprod  28650  fprodntriv  28651  prodss  28656  fprodn0  28686  fprod2dlem  28687  mpteq12d  28779  setinds2  28789  dfon2lem1  28792  dfon2lem3  28794  wfisg  28866  wfis2g  28870  trpredmintr  28891  frinsg  28902  frins2g  28906  frins2  28907  nfwrecs  28915  wfr3g  28919  frr3g  28963  wl-equsb3  29581  wl-sb8eut  29599  ptrest  29625  heicant  29626  mbfposadd  29639  itgabsnc  29661  itggt0cn  29664  ftc1anclem5  29671  finminlem  29713  upixp  29823  indexa  29827  indexdom  29828  filbcmb  29834  sdclem2  29838  sdclem1  29839  fdc1  29842  totbndbnd  29888  sbcalf  30120  sbcexf  30121  scottexf  30180  scott0f  30181  prtlem5  30201  mzpexpmpt  30281  eq0rabdioph  30314  rexrabdioph  30331  rexfrabdioph  30332  elnn0rabdioph  30340  dvdsrabdioph  30347  fphpd  30354  monotuz  30481  monotoddzz  30483  oddcomabszz  30484  setindtr  30570  dford4  30575  wdom2d2  30581  aomclem6  30609  aomclem8  30611  flcidc  30728  areaquad  30789  pm10.12  30841  19.31vv  30867  aaanv  30872  pm11.57  30873  pm11.58  30874  pm11.59  30875  pm11.71  30881  axc11next  30891  pm13.192  30895  pm14.12  30906  evth2f  30968  elunif  30969  fvelrnbf  30971  evthf  30980  fnchoice  30982  sumpair  30988  rfcnnnub  30989  refsum2cn  30991  elabrexg  31012  suprnmpt  31029  monoords  31073  fzisoeu  31077  upbdrech  31082  ssfiunibd  31086  iccshift  31122  iooshift  31126  icoiccdif  31128  fmul01  31130  fmuldfeqlem1  31132  fmuldfeq  31133  fmul01lt1lem1  31134  fmul01lt1lem2  31135  fmul01lt1  31136  infrglb  31140  climexp  31147  climsuse  31150  climrecf  31151  climinff  31153  climaddf  31157  mullimc  31158  ellimcabssub0  31159  islptre  31161  climf  31164  mullimcf  31165  rexlim2d  31167  idlimc  31168  limcperiod  31170  limcrecl  31171  sumnnodd  31172  islpcn  31181  limsupre  31183  limcleqr  31186  neglimc  31189  addlimc  31190  0ellimcdiv  31191  limclner  31193  cncfshift  31212  cncfperiod  31217  icccncfext  31226  cncficcgt0  31227  cncfiooicclem1  31232  cncfiooicc  31233  cncfioobd  31236  fperdvper  31248  dvbdfbdioolem1  31258  ioodvbdlimc1lem1  31261  iblsplitf  31288  iblspltprt  31291  itgioocnicc  31295  iblcncfioo  31296  itgspltprt  31297  itgiccshift  31298  itgperiod  31299  stoweidlem3  31303  stoweidlem14  31314  stoweidlem17  31317  stoweidlem19  31319  stoweidlem20  31320  stoweidlem26  31326  stoweidlem27  31327  stoweidlem28  31328  stoweidlem29  31329  stoweidlem31  31331  stoweidlem34  31334  stoweidlem35  31335  stoweidlem36  31336  stoweidlem39  31339  stoweidlem42  31342  stoweidlem43  31343  stoweidlem44  31344  stoweidlem46  31346  stoweidlem48  31348  stoweidlem49  31349  stoweidlem50  31350  stoweidlem51  31351  stoweidlem52  31352  stoweidlem53  31353  stoweidlem54  31354  stoweidlem56  31356  stoweidlem57  31357  stoweidlem59  31359  stoweidlem60  31360  stoweidlem61  31361  stoweidlem62  31362  stoweid  31363  wallispilem3  31367  stirlinglem13  31386  stirling  31389  dirkercncflem2  31404  fourierdlem15  31422  fourierdlem16  31423  fourierdlem21  31428  fourierdlem22  31429  fourierdlem31  31438  fourierdlem34  31441  fourierdlem39  31446  fourierdlem42  31449  fourierdlem45  31452  fourierdlem48  31455  fourierdlem50  31457  fourierdlem51  31458  fourierdlem53  31460  fourierdlem62  31469  fourierdlem68  31475  fourierdlem69  31476  fourierdlem71  31478  fourierdlem73  31480  fourierdlem77  31484  fourierdlem79  31486  fourierdlem80  31487  fourierdlem81  31488  fourierdlem82  31489  fourierdlem83  31490  fourierdlem86  31493  fourierdlem87  31494  fourierdlem89  31496  fourierdlem91  31498  fourierdlem92  31499  fourierdlem93  31500  fourierdlem94  31501  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  rexsb  31640  rmoanim  31651  2reu4a  31661  ffnafv  31723  opeliun2xp  31986  cbvmpt2x2  31989  ovmpt2rdx  31993  ssralv2  32380  tratrb  32386  iunconlem2  32815  bnj919  32904  bnj1146  32929  bnj1379  32968  bnj1385  32970  bnj1400  32973  bnj1476  32984  bnj1534  32990  bnj1542  32994  bnj110  32995  bnj121  33007  bnj124  33008  bnj130  33011  bnj207  33018  bnj571  33043  bnj605  33044  bnj580  33050  bnj607  33053  bnj611  33055  bnj873  33061  bnj849  33062  bnj900  33066  bnj916  33070  bnj1000  33078  bnj964  33080  bnj981  33087  bnj985  33090  bnj1014  33097  bnj1123  33121  bnj1128  33125  bnj1228  33146  bnj1204  33147  bnj1279  33153  bnj1307  33158  bnj1321  33162  bnj1388  33168  bnj1398  33169  bnj1408  33171  bnj1417  33176  bnj1444  33178  bnj1445  33179  bnj1446  33180  bnj1449  33183  bnj1467  33189  bnj1489  33191  bnj1312  33193  bnj1497  33195  bnj1518  33199  bnj1525  33204  bnj1529  33205  bj-nexdvt  33333  bj-spimvv  33364  bj-spimevv  33365  bj-chvarvv  33369  bj-cbv3v2  33371  bj-cbvalvv  33380  bj-cbvexvv  33381  bj-cbvaldv  33382  bj-cbval2v  33384  bj-cbval2vv  33386  bj-cbvex2vv  33387  bj-cbvaldvav  33388  bj-cbvexdvav  33389  bj-drnf2v  33410  bj-abbi  33442  bj-abbidv  33446  bj-axrep1  33455  bj-axrep2  33456  bj-axrep3  33457  bj-axrep4  33458  bj-axrep5  33459  bj-axsep  33460  ax11-pm2  33490  bj-clelsb3  33505  bj-nfcjust  33507  bj-ceqsalv  33540  bj-vtocl  33562  bj-inrab2  33577  fsumshftd  33754  fsumshftdOLD  33755  riotasv2d  33760  riotasv2s  33761  riotasv3d  33763  glbconxN  34174  pmapglbx  34565  pmapglb2xN  34568  cdleme26ee  35156  cdleme31sn  35176  cdleme31sn1  35177  cdlemefr29exN  35198  cdlemefs32sn1aw  35210  cdleme43fsv1snlem  35216  cdleme41sn3a  35229  cdleme32fva  35233  cdleme32d  35240  cdleme32f  35242  cdleme40m  35263  cdleme40n  35264  cdleme42b  35274  cdlemk36  35709  cdlemk38  35711  cdlemkid  35732  cdlemk19x  35739  cdlemk11t  35742  dihvalcqpre  36032  mapdheq  36525  hdmap1eq  36599  hdmapval2lem  36631
  Copyright terms: Public domain W3C validator