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

Theorem nfv 1692
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 1689 . 2  |-  ( ph  ->  A. x ph )
21nfi 1608 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-5 1689
This theorem depends on definitions:  df-bi 185  df-nf 1602
This theorem is referenced by:  nfvd  1693  nexdv  1868  dvelimhw  1939  19.21vOLD  1965  19.23vOLD  1966  pm11.53  1967  19.36vOLD  1968  19.36aivOLD  1969  19.12vv  1970  eeanv  1972  eeeanv  1973  spimv  1993  spimev  1994  chvarv  1998  cbvalv  2007  cbvexv  2008  cbvald  2009  cbval2  2011  cbvex2OLD  2013  cbval2v  2014  cbvex2v  2015  cbvaldva  2016  cbvexdva  2017  axc9lem2  2024  axc16i  2048  dvelimnf  2065  cleljustALT  2094  sbiedv  2136  equsb3lem  2159  equsb3  2160  equsb3ALT  2161  elsb3  2162  elsb4  2163  sbhb  2166  sbnf2  2167  sbcom2  2173  sbcom4  2174  dfsb7  2183  sbid2v  2185  sbel2x  2187  sbco4lem  2193  sbco4  2194  2sb8e  2195  exsb  2196  euf  2276  mo2  2277  nfeud2  2280  eubidv  2288  mobidv  2289  sb8eu  2302  sb8euOLD  2303  mo3OLD  2308  euexALT  2312  eu5OLD  2314  euorv  2316  sbmo  2319  mo4f  2320  mo4  2321  morimvOLD  2326  moanimv  2336  euanv  2339  mopickOLD  2341  moexexv  2348  2mo  2357  2moOLD  2358  2mos  2359  2eu4OLD  2365  2eu6  2367  2eu6OLD  2368  bm1.1  2424  bm1.1OLD  2425  cleqh  2556  eqsb3lem  2560  eqsb3  2561  clelsb3  2562  abbiOLD  2573  abbidv  2577  cbvabv  2584  clelab  2585  clelabOLD  2586  nfcjust  2590  nfcv  2603  nfeqd  2610  nfeld  2611  nfabd2  2624  dvelimdc  2626  cleqfOLD  2631  sbabel  2634  sbabelOLD  2635  r19.21vOLD  2847  ralimdvaOLD  2850  ralrimivOLD  2854  ralrimdvOLD  2858  ralbidvaOLD  2878  ralbidvOLD  2881  2ralbida  2882  2ralbidvaOLD  2884  reximdvaiOLD  2914  r19.23vOLD  2922  rexlimivOLD  2928  rexlimdvOLD  2932  rexbidvaALT  2950  rexbidvALT  2953  r19.29af  2981  r19.29an  2982  r19.29a  2983  r19.37av  2991  r19.41v  2994  reean  3008  reeanv  3009  reubidva  3025  rmobidva  3030  cbvralf  3062  cbvreu  3066  cbvralv  3068  cbvrexv  3069  cbvreuv  3070  cbvrmov  3071  cbvralsv  3079  cbvrexsv  3080  sbralie  3081  cbvrab  3091  cbvrabv  3092  issetf  3098  ceqsalv  3121  ceqsralv  3122  ceqsexv  3130  ceqsex2  3131  ceqsex2v  3132  vtocld  3143  vtocl  3145  vtoclg  3151  vtocl2g  3155  vtoclga  3157  vtocl2gaf  3158  vtocl2ga  3159  vtocl3gaf  3160  vtocl3ga  3161  spcimdv  3175  spcgv  3178  spcegv  3179  rspct  3187  rspc  3188  rspce  3189  rspcv  3190  rspcev  3194  rspc2v  3203  eqvincf  3211  ceqsexgv  3216  elabgt  3227  elab  3230  elabg  3231  elab3g  3236  elrab3t  3240  elrab  3241  ralab2  3248  rexab2  3250  mob2  3263  mob  3265  reu2  3271  reu2eqd  3280  nfcdeq  3308  sbcco  3334  sbcco2  3335  cbvsbcv  3341  sbcieg  3344  sbcie2g  3345  sbcied  3348  elrabsf  3350  sbcbidv  3370  sbcg  3385  sbc2iegf  3386  sbc2ie  3387  rmo2  3411  rmo3  3413  nfcsb1d  3432  nfcsbd  3435  csbiebt  3438  csbied  3445  csbie2t  3447  cbvralcsf  3450  cbvreucsf  3452  cbvrabcsf  3453  cbvralv2  3454  cbvrexv2  3455  dfss2f  3478  uniiunlem  3571  rspn0  3780  csbeq2dv  3818  sbcnestg  3824  sbnfc2  3837  sbss  3921  nfifd  3951  rabsnifsb  4080  euabsn  4084  nfuni  4237  nfunid  4238  eluniab  4242  nfint  4278  elintab  4279  rabasiun  4316  iineq2dv  4335  disjiun  4424  disjxun  4432  opabbidv  4497  nfopab  4499  cbvopab  4502  cbvopabv  4503  cbvopab1  4504  cbvopab2  4505  cbvopab1s  4506  cbvopab1v  4507  mpteq12f  4510  mpteq2dva  4520  cbvmpt  4524  axrep1  4546  axrep2  4547  axrep3  4548  axrep4  4549  axrep5  4550  zfrepclf  4551  axsep  4554  zfnuleu  4560  reusv2lem2  4636  reusv2lem3  4637  reusv2lem4  4638  reusv2  4640  reusv3  4642  reusv6OLD  4645  alxfr  4647  ralxfrALT  4653  copsex2t  4721  copsex2g  4722  opelopabaf  4758  nfso  4793  pofun  4803  nffr  4840  opeliunxp  5038  opeliunxp2  5128  ralxpf  5136  dfdmf  5183  dfrnf  5228  elrnmpt1  5238  asymref2  5371  intirr  5372  nfiotad  5541  cbviota  5543  cbviotav  5544  sb8iota  5545  iota2d  5563  iota2  5564  dffun6f  5589  fun11  5640  imadif  5650  funimaexg  5652  isarep1  5654  isarep2  5655  fv3  5866  tz6.12f  5871  tz6.12c  5872  opabiotafun  5916  funfv2f  5924  fvmptdf  5949  fvmptdv  5950  fvmptt  5953  fvopab5  5961  eqfnfv2f  5967  ralrnmpt  6022  f1ompt  6035  ffnfv  6039  ffnfvf  6040  fmptco  6046  elabrex  6137  dff13f  6149  fliftfun  6192  cbvriota  6249  cbvriotav  6250  riota2  6262  riota5f  6264  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  ovmpt3rab1  6516  ofrfval2  6539  onminex  6624  tfis  6671  tfis2  6673  tfisi  6675  tfinds  6676  tfindes  6679  peano5  6705  findes  6712  fun11iun  6742  abrexex2g  6759  opabex3d  6760  opabex3  6761  abrexex2  6763  dfoprab4f  6840  fmpt2x  6848  offval22  6861  ovmptss  6863  tposoprab  6990  fvmpt2curryd  6999  nfrecs  7043  tfr3  7067  nfrdg  7079  tz7.48-1  7107  tz7.49  7109  eqerlem  7342  erovlem  7406  mptelixpg  7505  boxcutc  7511  dom2lem  7554  xpf1o  7678  mapxpen  7682  nneneq  7699  pssnn  7737  findcard2  7759  ac6sfi  7763  fiint  7796  indexfi  7827  wdom2d  8006  ixpiunwdom  8017  sucprcregOLD  8026  cantnflem1  8108  r1val1  8204  rankuni2b  8271  scottexs  8305  scott0s  8306  dfac8clem  8413  acni2  8427  aceq1  8498  dfac5lem5  8508  kmlem15  8544  infpssrlem4  8686  fin23lem27  8708  hsmexlem2  8807  hsmexlem4  8809  axcc3  8818  domtriomlem  8822  axdc3lem2  8831  axdc3lem4  8833  axdc4lem  8835  ac6num  8859  ac6c4  8861  zorn2lem4  8879  zorn2lem5  8880  iunfo  8914  iundom2g  8915  uniimadomf  8920  konigthlem  8943  axrepndlem2  8968  axunnd  8971  axpowndlem2  8973  axpowndlem2OLD  8974  axpowndlem4  8977  axregndlem2  8980  axacndlem5  8989  zfcndrep  8992  zfcndpow  8994  zfcndinf  8996  zfcndac  8997  pwfseqlem4a  9039  pwfseqlem4  9040  tskuni  9161  gruiin  9188  grothprim  9212  reclem2pr  9426  dedekind  9744  dedekindle  9745  fimaxre3  10495  uzindOLD  10960  nn0ind-raph  10966  uzind4s  11147  nnwof  11154  lbzbi  11176  fzrevral  11768  rabssnn0fi  12071  fsuppmapnn0fiublem  12072  fsuppmapnn0fiub  12073  fsuppmapnn0fiubex  12074  seqof2  12141  rlim2  13295  ello1mpt  13320  climeu  13354  o1compt  13386  summolem2a  13513  zsum  13516  sumss  13522  sumss2  13524  fsumcvg2  13525  fsum2dlem  13561  fsum00  13588  o1fsum  13603  prmind2  14102  iserodd  14233  pcmpt  14285  pcmptdvds  14287  mreexexd  14919  catpropd  14978  invfuc  15214  natpropd  15216  fucpropd  15217  acsmapd  15679  gsumsnd  16850  gsumsnf  16851  gsumunsnfd  16854  gsummptf1o  16861  gsummpt1n0  16863  gsum2d2lem  16872  gsumcom2  16874  gsummptnn0fz  16885  gsummptnn0fzv  16886  dprdwdOLD2  16916  dprdwdOLD  16922  dprd2d2  16964  gsummoncoe1  18217  gsumply1eq  18218  mdetralt2  18981  mdetunilem2  18985  madugsum  19015  gsummatr01lem4  19030  cpmatmcllem  19089  pmatcollpwfi  19153  cayleyhamilton1  19263  neiptopnei  19503  neiptopreu  19504  neitr  19551  fiuncmp  19774  bwthOLD  19781  iunconlem  19798  iuncon  19799  2ndcdisj  19827  dissnlocfin  19900  elptr2  19945  ptbasfi  19952  ptcld  19984  ptcldmpt  19985  ptclsg  19986  ptcnplem  19992  ptcnp  19993  cnmpt11  20034  cnmpt21  20042  cnmptcom  20049  imasnopn  20061  imasncld  20062  imasncls  20063  xkocnv  20185  elmptrab  20198  isfildlem  20228  alexsubALTlem3  20419  cnextfvval  20435  utopsnneiplem  20620  isucn2  20652  cfilucfilOLD  20942  cfilucfil  20943  blval2  20948  restmetu  20960  ovoliunlem3  21785  ovoliun  21786  ovoliun2  21787  ovoliunnul  21788  finiunmbl  21824  volfiniun  21827  iundisj  21828  iunmbl  21833  voliun  21834  iunmbl2  21837  mbfeqalem  21919  mbfsup  21941  mbfinf  21942  mbflim  21945  itg2splitlem  22025  itg2split  22026  isibl2  22043  cbvitg  22052  itgeqa  22090  itgss3  22091  itgfsum  22103  itgabs  22111  itggt0  22118  itgcn  22119  limcmpt  22157  limciun  22168  dvmptfsum  22246  dvlipcn  22265  dvfsumlem2  22298  dvfsumlem4  22300  dvfsumrlim  22302  dvfsum2  22305  itgsubst  22320  coeeq2  22509  dgrle  22510  ulmss  22661  leibpi  23142  rlimcnp  23164  rlimcnp2  23165  o1cxp  23173  fsumdvdscom  23330  lgseisenlem2  23494  dchrisumlema  23542  dchrisumlem2  23544  dchrisumlem3  23545  istrkg2ld  23727  mptelee  24067  ex-natded9.26  25009  isch3  26028  atom1d  27141  chirred  27183  spc2ed  27241  19.9d2r  27247  clelsb3f  27248  mo5f  27252  rmoeq  27255  rmo4fOLD  27264  rmo4f  27265  foresf1o  27272  elabreximdv  27278  rabss3d  27281  iuninc  27297  cbvdisjf  27303  disjorf  27309  disjabrex  27312  iundisjf  27317  disjunsn  27322  dfrel4  27323  dfimafnf  27342  suppss2f  27346  fimarab  27352  cbvmptf  27363  feqmptdf  27370  fmptcof2  27371  ofpreima  27376  funcnvmptOLD  27378  funcnv5mpt  27380  funcnv4mpt  27381  cnvoprab  27415  f1od2  27416  fpwrelmap  27425  xrofsup  27451  iundisjfi  27470  nnindf  27480  nn0min  27481  2sqmo  27507  isarchiofld  27677  reff  27712  locfinreflem  27713  cmpcref  27723  ordtconlem1  27776  qqhval2  27833  esumeq12dva  27915  esumeq2dv  27921  esumc  27932  esumadd  27934  gsumesum  27937  esumlub  27938  esumpr  27943  esumfzf  27945  esumfsup  27946  esumpcvgval  27954  esumpmono  27955  esumcocn  27956  hasheuni  27961  esumcvg  27962  measvunilem  28053  measvunilem0  28054  measvuni  28055  measiuns  28058  measiun  28059  measinblem  28061  voliune  28071  volfiniune  28072  volmeas  28073  ddemeas  28078  oms0  28136  eulerpartlemgvv  28185  dstrvprob  28280  ballotlemodife  28306  lgamgulmlem2  28442  lgamgulmlem6  28446  cvmcov  28578  untsucf  28952  nfcprod1  29014  nfcprod  29015  prodmolem2a  29038  zprod  29041  fprod  29045  fprodntriv  29046  prodss  29051  fprodn0  29081  fprod2dlem  29082  mpteq12d  29174  setinds2  29184  dfon2lem1  29187  dfon2lem3  29189  wfisg  29261  wfis2g  29265  trpredmintr  29286  frinsg  29297  frins2g  29301  frins2  29302  nfwrecs  29310  wl-equsb3  29976  wl-sb8eut  29994  ptrest  30020  heicant  30021  mbfposadd  30034  itgabsnc  30056  itggt0cn  30059  ftc1anclem5  30066  finminlem  30108  upixp  30192  indexa  30196  indexdom  30197  filbcmb  30203  sdclem2  30207  sdclem1  30208  fdc1  30211  totbndbnd  30257  sbcalf  30489  sbcexf  30490  scottexf  30548  scott0f  30549  prtlem5  30569  mzpexpmpt  30649  eq0rabdioph  30682  rexrabdioph  30699  rexfrabdioph  30700  elnn0rabdioph  30708  dvdsrabdioph  30715  fphpd  30722  monotuz  30849  monotoddzz  30851  oddcomabszz  30852  setindtr  30938  dford4  30943  wdom2d2  30949  aomclem6  30977  aomclem8  30979  flcidc  31096  areaquad  31157  aaanv  31245  pm11.57  31246  pm11.58  31247  pm11.59  31248  pm11.71  31254  pm13.192  31268  pm14.12  31279  evth2f  31341  elunif  31342  fvelrnbf  31344  evthf  31353  fnchoice  31355  sumpair  31361  rfcnnnub  31362  refsum2cn  31364  elabrexg  31384  suprnmpt  31401  upbdrech  31454  ssfiunibd  31458  iccshift  31494  iooshift  31498  fmul01  31502  fmuldfeqlem1  31504  fmuldfeq  31505  fmul01lt1lem1  31506  fmul01lt1lem2  31507  fmul01lt1  31508  infrglb  31512  climexp  31519  climsuse  31522  climrecf  31523  climinff  31525  climaddf  31529  mullimc  31530  ellimcabssub0  31531  islptre  31533  climf  31536  mullimcf  31537  rexlim2d  31539  idlimc  31540  limcperiod  31542  limcrecl  31543  sumnnodd  31544  islpcn  31553  limsupre  31555  limcleqr  31558  neglimc  31561  addlimc  31562  0ellimcdiv  31563  limclner  31565  cncfshift  31583  icccncfext  31597  cncficcgt0  31598  cncfiooicclem1  31603  cncfiooicc  31604  cncfioobd  31607  iblsplitf  31659  iblspltprt  31662  itgioocnicc  31666  iblcncfioo  31667  itgspltprt  31668  itgperiod  31670  stoweidlem3  31674  stoweidlem14  31685  stoweidlem17  31688  stoweidlem19  31690  stoweidlem20  31691  stoweidlem26  31697  stoweidlem27  31698  stoweidlem28  31699  stoweidlem29  31700  stoweidlem31  31702  stoweidlem34  31705  stoweidlem35  31706  stoweidlem36  31707  stoweidlem39  31710  stoweidlem42  31713  stoweidlem43  31714  stoweidlem44  31715  stoweidlem46  31717  stoweidlem48  31719  stoweidlem49  31720  stoweidlem50  31721  stoweidlem51  31722  stoweidlem52  31723  stoweidlem53  31724  stoweidlem54  31725  stoweidlem56  31727  stoweidlem57  31728  stoweidlem59  31730  stoweidlem60  31731  stoweidlem61  31732  stoweidlem62  31733  stoweid  31734  wallispilem3  31738  stirlinglem13  31757  stirling  31760  fourierdlem16  31794  fourierdlem21  31799  fourierdlem22  31800  fourierdlem31  31809  fourierdlem39  31817  fourierdlem48  31826  fourierdlem51  31829  fourierdlem53  31831  fourierdlem68  31846  fourierdlem69  31847  fourierdlem71  31849  fourierdlem73  31851  fourierdlem77  31855  fourierdlem80  31858  fourierdlem81  31859  fourierdlem82  31860  fourierdlem83  31861  fourierdlem86  31864  fourierdlem87  31865  fourierdlem89  31867  fourierdlem91  31869  fourierdlem93  31871  fourierdlem94  31872  fourierdlem103  31881  fourierdlem104  31882  fourierdlem112  31890  fourierdlem113  31891  rexsb  32011  rmoanim  32022  2reu4a  32032  ffnafv  32094  2zrngagrp  32456  2zrngmmgm  32459  opeliun2xp  32650  cbvmpt2x2  32653  ovmpt2rdx  32657  ssralv2  33029  tratrb  33035  iunconlem2  33463  bnj919  33553  bnj1146  33578  bnj1379  33617  bnj1385  33619  bnj1400  33622  bnj1476  33633  bnj1534  33639  bnj1542  33643  bnj110  33644  bnj121  33656  bnj124  33657  bnj130  33660  bnj207  33667  bnj571  33692  bnj605  33693  bnj580  33699  bnj607  33702  bnj611  33704  bnj873  33710  bnj849  33711  bnj900  33715  bnj916  33719  bnj1000  33727  bnj964  33729  bnj981  33736  bnj985  33739  bnj1014  33746  bnj1123  33770  bnj1128  33774  bnj1228  33795  bnj1204  33796  bnj1279  33802  bnj1307  33807  bnj1321  33811  bnj1388  33817  bnj1398  33818  bnj1408  33820  bnj1417  33825  bnj1444  33827  bnj1445  33828  bnj1446  33829  bnj1449  33832  bnj1467  33838  bnj1489  33840  bnj1312  33842  bnj1497  33844  bnj1518  33848  bnj1525  33853  bnj1529  33854  bj-nexdvt  33986  bj-spimvv  34017  bj-spimevv  34018  bj-chvarvv  34022  bj-cbv3v2  34024  bj-cbvalvv  34033  bj-cbvexvv  34034  bj-cbvaldv  34035  bj-cbval2v  34037  bj-cbval2vv  34039  bj-cbvex2vv  34040  bj-cbvaldvav  34041  bj-cbvexdvav  34042  bj-drnf2v  34062  bj-abbi  34094  bj-abbidv  34098  bj-axrep1  34107  bj-axrep2  34108  bj-axrep3  34109  bj-axrep4  34110  bj-axrep5  34111  bj-axsep  34112  ax11-pm2  34142  bj-clelsb3  34157  bj-nfcjust  34159  bj-ceqsalv  34192  bj-vtocl  34214  bj-inrab2  34229  fsumshftd  34405  fsumshftdOLD  34406  riotasv2d  34411  riotasv2s  34412  riotasv3d  34414  glbconxN  34825  pmapglbx  35216  pmapglb2xN  35219  cdleme26ee  35809  cdleme31sn  35829  cdleme31sn1  35830  cdlemefr29exN  35851  cdlemefs32sn1aw  35863  cdleme43fsv1snlem  35869  cdleme41sn3a  35882  cdleme32fva  35886  cdleme32d  35893  cdleme32f  35895  cdleme40m  35916  cdleme40n  35917  cdleme42b  35927  cdlemk36  36362  cdlemk38  36364  cdlemkid  36385  cdlemk19x  36392  cdlemk11t  36395  dihvalcqpre  36685  mapdheq  37178  hdmap1eq  37252  hdmapval2lem  37284  cotr2g  37462  frege70  37613  frege72  37615
  Copyright terms: Public domain W3C validator