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

Theorem nfv 1674
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 1671 . 2  |-  ( ph  ->  A. x ph )
21nfi 1597 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-5 1671
This theorem depends on definitions:  df-bi 185  df-nf 1591
This theorem is referenced by:  nfvd  1675  nexdv  1820  dvelimhw  1890  19.21v  1918  19.23v  1919  pm11.53  1921  19.27v  1922  19.28v  1923  19.36v  1924  19.36aiv  1925  19.12vv  1926  19.37v  1927  19.41v  1929  19.42v  1933  eeanv  1941  eeeanv  1942  spimv  1962  spimev  1963  chvarv  1967  cbvalv  1980  cbvexv  1981  cbvald  1982  cbval2  1984  cbvex2OLD  1986  cbval2v  1987  cbvex2v  1988  cbvaldva  1989  cbvexdva  1990  axc9lem2  1997  axc16i  2021  dvelimnf  2038  cleljustALT  2067  sbiedv  2111  equsb3lem  2143  equsb3  2144  equsb3ALT  2145  elsb3  2146  elsb4  2147  sbhb  2150  sbnf2  2151  sbnf2OLD  2152  sbcom2  2158  sbcom4  2160  dfsb7  2172  sbid2v  2174  sbel2x  2176  sbco4lem  2185  sbco4  2186  2sb8e  2187  exsb  2188  euf  2270  eufOLD  2271  mo2  2272  nfeud2  2275  eubidv  2283  mobidv  2284  nfeud2OLD  2287  sb8eu  2299  sb8euOLD  2300  sb8euOLDOLD  2301  mo3OLD  2306  moOLD  2312  euexALT  2313  eu5OLD  2316  euorv  2318  sbmo  2322  mo4f  2323  mo4  2324  morimvOLD  2329  moanimOLD  2340  moanimv  2341  euanv  2345  mopickOLD  2347  mopickOLDOLD  2348  moexexv  2358  2mo  2367  2moOLD  2368  2moOLDOLD  2369  2mos  2370  2eu4OLD  2376  2eu6  2378  2eu6OLD  2379  bm1.1  2434  bm1.1OLD  2435  cleqh  2566  eqsb3lem  2570  eqsb3  2571  clelsb3  2572  abbiOLD  2583  abbidv  2587  cbvabv  2594  clelab  2595  clelabOLD  2596  nfcjust  2600  nfcv  2613  nfeqd  2620  nfeld  2621  nfabd2  2633  dvelimdc  2635  cleqfOLD  2640  sbabel  2643  ralrimivOLD  2821  ralimdvaOLD  2825  ralbidvaOLD  2838  ralbidvOLD  2840  rexbidva  2842  rexbidv  2844  2ralbida  2858  2ralbidva  2859  r19.21v  2899  ralrimdv  2901  reximdvai  2922  r19.23v  2929  rexlimiv  2931  rexlimdv  2936  r19.29af  2957  r19.29a  2958  r19.37av  2966  r19.41v  2969  reean  2983  reeanv  2984  reubidva  3000  rmobidva  3005  cbvralf  3037  cbvreu  3041  cbvralv  3043  cbvrexv  3044  cbvreuv  3045  cbvrmov  3046  cbvralsv  3054  cbvrexsv  3055  sbralie  3056  cbvrab  3066  cbvrabv  3067  issetf  3073  ceqsalv  3096  ceqsralv  3097  ceqsexv  3105  ceqsex2  3106  ceqsex2v  3107  vtocld  3118  vtocl  3120  vtoclg  3126  vtocl2g  3130  vtoclga  3132  vtocl2gaf  3133  vtocl2ga  3134  vtocl3gaf  3135  vtocl3ga  3136  spcimdv  3150  spcgv  3153  spcegv  3154  rspct  3162  rspc  3163  rspce  3164  rspcv  3165  rspcev  3169  rspc2v  3176  eqvincf  3184  ceqsexgv  3189  elabgt  3200  elab  3203  elabg  3204  elab3g  3209  elrab3t  3213  elrab  3214  ralab2  3221  rexab2  3223  mob2  3236  mob  3238  reu2  3244  reu2eqd  3253  nfcdeq  3281  sbcco  3307  sbcco2  3308  cbvsbcv  3314  sbcieg  3317  sbcie2g  3318  sbcied  3321  elrabsf  3323  sbcbidv  3343  sbcg  3358  sbc2iegf  3359  sbc2ie  3360  rmo2  3381  rmo3  3383  nfcsb1d  3400  nfcsbd  3403  csbiebt  3406  csbied  3412  csbie2t  3414  cbvralcsf  3417  cbvreucsf  3419  cbvrabcsf  3420  cbvralv2  3421  cbvrexv2  3422  dfss2f  3445  uniiunlem  3538  rspn0  3747  csbeq2dv  3785  sbcnestg  3791  sbnfc2  3804  sbss  3887  nfifd  3915  rabsnifsb  4041  euabsn  4045  nfuni  4195  nfunid  4196  eluniab  4200  nfint  4236  elintab  4237  iineq2dv  4291  disjiun  4380  disjxun  4388  opabbidv  4453  nfopab  4455  cbvopab  4458  cbvopabv  4459  cbvopab1  4460  cbvopab2  4461  cbvopab1s  4462  cbvopab1v  4463  mpteq12f  4466  mpteq2dva  4476  cbvmpt  4480  axrep1  4502  axrep2  4503  axrep3  4504  axrep4  4505  axrep5  4506  zfrepclf  4507  axsep  4510  zfnuleu  4516  reusv2lem2  4592  reusv2lem3  4593  reusv2lem4  4594  reusv2  4596  reusv3  4598  reusv6OLD  4601  alxfr  4603  ralxfrALT  4609  copsex2t  4676  copsex2g  4677  opelopabaf  4710  nfso  4745  pofun  4755  nffr  4792  opeliunxp  4988  opeliunxp2  5076  ralxpf  5084  dfdmf  5131  dfrnf  5176  elrnmpt1  5186  asymref2  5313  intirr  5314  nfiotad  5482  cbviota  5484  cbviotav  5485  sb8iota  5486  iota2d  5504  iota2  5505  dffun6f  5530  fun11  5581  imadif  5591  funimaexg  5593  isarep1  5595  isarep2  5596  fv3  5802  tz6.12f  5807  tz6.12c  5808  opabiotafun  5851  funfv2f  5859  fvmptdf  5884  fvmptdv  5885  fvmptt  5888  fvopab5  5894  eqfnfv2f  5900  ralrnmpt  5951  f1ompt  5964  ffnfv  5968  ffnfvf  5969  fmptco  5975  elabrex  6059  dff13f  6072  fliftfun  6104  cbvriota  6161  cbvriotav  6162  riota2  6174  riota5f  6176  nfoprab  6237  oprabbidv  6239  mpt2eq123  6244  cbvoprab1  6257  cbvoprab2  6258  cbvoprab12  6259  cbvoprab12v  6260  cbvoprab3  6261  cbvoprab3v  6262  cbvmpt2x  6263  ralrnmpt2  6305  ovmpt2dx  6317  ovmpt2df  6322  ovmpt2dv  6323  ov3  6327  ofrfval2  6437  onminex  6518  tfis  6565  tfis2  6567  tfisi  6569  tfinds  6570  tfindes  6573  peano5  6599  findes  6606  fun11iun  6637  abrexex2g  6654  opabex3d  6655  opabex3  6656  abrexex2  6658  dfoprab4f  6732  fmpt2x  6740  offval22  6752  ovmptss  6754  tposoprab  6881  fvmpt2curryd  6890  nfrecs  6934  tfr3  6958  nfrdg  6970  tz7.48-1  6998  tz7.49  7000  eqerlem  7233  erovlem  7296  mptelixpg  7400  boxcutc  7406  dom2lem  7449  xpf1o  7573  mapxpen  7577  nneneq  7594  pssnn  7632  findcard2  7653  ac6sfi  7657  fiint  7689  indexfi  7720  wdom2d  7896  ixpiunwdom  7907  sucprcregOLD  7916  cantnflem1  7998  r1val1  8094  rankuni2b  8161  scottexs  8195  scott0s  8196  dfac8clem  8303  acni2  8317  aceq1  8388  dfac5lem5  8398  kmlem15  8434  infpssrlem4  8576  fin23lem27  8598  hsmexlem2  8697  hsmexlem4  8699  axcc3  8708  domtriomlem  8712  axdc3lem2  8721  axdc3lem4  8723  axdc4lem  8725  ac6num  8749  ac6c4  8751  zorn2lem4  8769  zorn2lem5  8770  iunfo  8804  iundom2g  8805  uniimadomf  8810  konigthlem  8833  axrepndlem2  8858  axunnd  8861  axpowndlem2  8863  axpowndlem2OLD  8864  axpowndlem4  8867  axregndlem2  8870  axacndlem5  8879  zfcndrep  8882  zfcndpow  8884  zfcndinf  8886  zfcndac  8887  pwfseqlem4a  8929  pwfseqlem4  8930  tskuni  9051  gruiin  9078  grothprim  9102  reclem2pr  9318  dedekind  9634  dedekindle  9635  fimaxre3  10380  uzindOLD  10837  nn0ind-raph  10843  uzind4s  11015  nnwof  11022  lbzbi  11044  fzrevral  11645  seqof2  11965  rlim2  13076  ello1mpt  13101  climeu  13135  o1compt  13167  summolem2a  13294  zsum  13297  sumss  13303  sumss2  13305  fsumcvg2  13306  fsum2dlem  13339  fsum00  13363  o1fsum  13378  prmind2  13876  iserodd  14004  pcmpt  14056  pcmptdvds  14058  mreexexd  14688  catpropd  14750  invfuc  14986  natpropd  14988  fucpropd  14989  acsmapd  15450  gsummptshft  16534  gsummpt1n0  16561  gsum2d2lem  16570  gsumcom2  16572  dprdwd  16600  dprdwdOLD  16606  dprd2d2  16648  mdetralt2  18531  mdetunilem2  18535  madugsum  18565  gsummatr01lem4  18580  neiptopnei  18852  neiptopreu  18853  neitr  18900  fiuncmp  19123  bwthOLD  19130  iunconlem  19147  iuncon  19148  2ndcdisj  19176  elptr2  19263  ptbasfi  19270  ptcld  19302  ptcldmpt  19303  ptclsg  19304  ptcnplem  19310  ptcnp  19311  cnmpt11  19352  cnmpt21  19360  cnmptcom  19367  imasnopn  19379  imasncld  19380  imasncls  19381  xkocnv  19503  elmptrab  19516  isfildlem  19546  alexsubALTlem3  19737  cnextfvval  19753  utopsnneiplem  19938  isucn2  19970  cfilucfilOLD  20260  cfilucfil  20261  blval2  20266  restmetu  20278  ovoliunlem3  21103  ovoliun  21104  ovoliun2  21105  ovoliunnul  21106  finiunmbl  21141  volfiniun  21144  iundisj  21145  iunmbl  21150  voliun  21151  iunmbl2  21154  mbfeqalem  21236  mbfsup  21258  mbfinf  21259  mbflim  21262  itg2splitlem  21342  itg2split  21343  isibl2  21360  cbvitg  21369  itgeqa  21407  itgss3  21408  itgfsum  21420  itgabs  21428  itggt0  21435  itgcn  21436  limcmpt  21474  limciun  21485  dvmptfsum  21563  dvlipcn  21582  dvfsumlem2  21615  dvfsumlem4  21617  dvfsumrlim  21619  dvfsum2  21622  itgsubst  21637  coeeq2  21826  dgrle  21827  ulmss  21978  leibpi  22453  rlimcnp  22475  rlimcnp2  22476  o1cxp  22484  fsumdvdscom  22641  lgseisenlem2  22805  dchrisumlema  22853  dchrisumlem2  22855  dchrisumlem3  22856  istrkg2ld  23038  tgldim0eq  23074  colline  23177  f1otrg  23252  mptelee  23276  ex-natded9.26  23761  isch3  24779  atom1d  25892  chirred  25934  spc2ed  25992  19.9d2r  25998  clelsb3f  25999  mo5f  26003  rmoeq  26006  rmo4fOLD  26015  rmo4f  26016  elabreximdv  26027  rabss3d  26030  iuninc  26045  cbvdisjf  26051  disjorf  26057  disjabrex  26060  iundisjf  26065  disjunsn  26070  dfrel4  26071  ssrelf  26079  dfimafnf  26084  suppss2f  26088  cbvmptf  26105  feqmptdf  26112  fmptcof2  26113  ofpreima  26118  funcnvmptOLD  26120  funcnv5mpt  26122  funcnv4mpt  26123  cnvoprab  26157  f1od2  26158  fcobijfs  26160  fpwrelmapffslem  26166  fpwrelmap  26167  xrofsup  26189  iundisjfi  26214  nnindf  26223  nn0min  26224  isarchi3  26338  gsummptf1o  26381  isarchiofld  26419  ordtconlem1  26488  qqhval2  26545  esumeq12dva  26622  esumeq2dv  26628  esumc  26639  esumadd  26641  gsumesum  26644  esumlub  26645  esumpr  26650  esumfzf  26652  esumfsup  26653  esumpcvgval  26661  esumpmono  26662  esumcocn  26663  hasheuni  26668  esumcvg  26669  measvunilem  26760  measvunilem0  26761  measvuni  26762  measiuns  26765  measiun  26766  measinblem  26768  voliune  26779  volfiniune  26780  volmeas  26781  ddemeas  26786  oms0  26844  eulerpartlemgvv  26893  eulerpart  26899  dstrvprob  26988  ballotlemodife  27014  lgamgulmlem2  27150  lgamgulmlem6  27154  cvmcov  27286  untsucf  27495  nfcprod1  27557  nfcprod  27558  prodmolem2a  27581  zprod  27584  fprod  27588  fprodntriv  27589  prodss  27594  fprodn0  27624  fprod2dlem  27625  mpteq12d  27717  setinds2  27727  dfon2lem1  27730  dfon2lem3  27732  wfisg  27804  wfis2g  27808  trpredmintr  27829  frinsg  27840  frins2g  27844  frins2  27845  nfwrecs  27853  wfr3g  27857  frr3g  27901  wl-equsb3  28518  wl-sb8eut  28536  ptrest  28563  heicant  28564  mbfposadd  28577  itgabsnc  28599  itggt0cn  28602  ftc1anclem5  28609  finminlem  28651  upixp  28761  indexa  28765  indexdom  28766  filbcmb  28772  sdclem2  28776  sdclem1  28777  fdc1  28780  totbndbnd  28826  sbcalf  29058  sbcexf  29059  scottexf  29118  scott0f  29119  prtlem5  29139  mzpexpmpt  29219  eq0rabdioph  29253  rexrabdioph  29270  rexfrabdioph  29271  elnn0rabdioph  29279  dvdsrabdioph  29286  fphpd  29293  monotuz  29420  monotoddzz  29422  oddcomabszz  29423  setindtr  29511  dford4  29516  wdom2d2  29522  aomclem6  29550  aomclem8  29552  flcidc  29669  areaquad  29730  pm10.12  29748  19.31vv  29774  aaanv  29779  pm11.57  29780  pm11.58  29781  pm11.59  29782  pm11.71  29788  axc11next  29798  pm13.192  29802  pm14.12  29813  evth2f  29875  elunif  29876  fvelrnbf  29878  evthf  29887  fnchoice  29889  sumpair  29895  rfcnnnub  29896  refsum2cn  29898  fmul01  29899  fmuldfeqlem1  29901  fmuldfeq  29902  fmul01lt1lem1  29903  fmul01lt1lem2  29904  fmul01lt1  29905  infrglb  29909  climexp  29916  climsuse  29919  climrecf  29920  climinff  29922  stoweidlem3  29936  stoweidlem14  29947  stoweidlem17  29950  stoweidlem19  29952  stoweidlem20  29953  stoweidlem26  29959  stoweidlem27  29960  stoweidlem28  29961  stoweidlem29  29962  stoweidlem31  29964  stoweidlem34  29967  stoweidlem35  29968  stoweidlem36  29969  stoweidlem39  29972  stoweidlem42  29975  stoweidlem43  29976  stoweidlem44  29977  stoweidlem46  29979  stoweidlem48  29981  stoweidlem49  29982  stoweidlem50  29983  stoweidlem51  29984  stoweidlem52  29985  stoweidlem53  29986  stoweidlem54  29987  stoweidlem56  29989  stoweidlem57  29990  stoweidlem59  29992  stoweidlem60  29993  stoweidlem61  29994  stoweidlem62  29995  stoweid  29996  wallispilem3  30000  stirlinglem13  30019  stirling  30022  rexsb  30130  rmoanim  30141  2reu4a  30151  ffnafv  30215  oprabv  30295  rabasiun  30368  opeliun2xp  30858  cbvmpt2x2  30864  ovmpt2rdx  30868  rabssnn0fi  30885  fsuppmapnn0fiublem  30936  fsuppmapnn0fiub  30937  fsuppmapnn0fiubex  30938  gsummptnn0fz  30947  gsummptnn0fzv  30948  gsummoncoe1  30985  gsumply1eq  30994  cpmatmcllem  31181  pmatcollpw3fi  31239  cayleyhamilton1  31347  ssralv2  31536  tratrb  31542  iunconlem2  31971  bnj919  32060  bnj1146  32085  bnj1379  32124  bnj1385  32126  bnj1400  32129  bnj1476  32140  bnj1534  32146  bnj1542  32150  bnj110  32151  bnj121  32163  bnj124  32164  bnj130  32167  bnj207  32174  bnj571  32199  bnj605  32200  bnj580  32206  bnj607  32209  bnj611  32211  bnj873  32217  bnj849  32218  bnj900  32222  bnj916  32226  bnj1000  32234  bnj964  32236  bnj981  32243  bnj985  32246  bnj1014  32253  bnj1123  32277  bnj1128  32281  bnj1228  32302  bnj1204  32303  bnj1279  32309  bnj1307  32314  bnj1321  32318  bnj1388  32324  bnj1398  32325  bnj1408  32327  bnj1417  32332  bnj1444  32334  bnj1445  32335  bnj1446  32336  bnj1449  32339  bnj1467  32345  bnj1489  32347  bnj1312  32349  bnj1497  32351  bnj1518  32355  bnj1525  32360  bnj1529  32361  bj-nexdvt  32487  bj-spimvv  32518  bj-spimevv  32519  bj-chvarvv  32523  bj-cbv3v2  32525  bj-cbvalvv  32534  bj-cbvexvv  32535  bj-cbvaldv  32536  bj-cbval2v  32538  bj-cbval2vv  32540  bj-cbvex2vv  32541  bj-cbvaldvav  32542  bj-cbvexdvav  32543  bj-drnf2v  32564  bj-abbi  32596  bj-abbidv  32600  bj-axrep1  32609  bj-axrep2  32610  bj-axrep3  32611  bj-axrep4  32612  bj-axrep5  32613  bj-axsep  32614  ax11-pm2  32644  bj-clelsb3  32659  bj-nfcjust  32661  bj-ceqsalv  32694  bj-vtocl  32716  bj-inrab2  32731  fsumshftd  32908  fsumshftdOLD  32909  riotasv2d  32914  riotasv2s  32915  riotasv3d  32917  glbconxN  33328  pmapglbx  33719  pmapglb2xN  33722  cdleme26ee  34310  cdleme31sn  34330  cdleme31sn1  34331  cdlemefr29exN  34352  cdlemefs32sn1aw  34364  cdleme43fsv1snlem  34370  cdleme41sn3a  34383  cdleme32fva  34387  cdleme32d  34394  cdleme32f  34396  cdleme40m  34417  cdleme40n  34418  cdleme42b  34428  cdlemk36  34863  cdlemk38  34865  cdlemkid  34886  cdlemk19x  34893  cdlemk11t  34896  dihvalcqpre  35186  mapdheq  35679  hdmap1eq  35753  hdmapval2lem  35785
  Copyright terms: Public domain W3C validator