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

Theorem nfv 1712
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 1709 . 2  |-  ( ph  ->  A. x ph )
21nfi 1628 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-5 1709
This theorem depends on definitions:  df-bi 185  df-nf 1622
This theorem is referenced by:  nfvd  1713  nexdv  1889  dvelimhw  1960  19.21vOLD  1986  19.23vOLD  1987  pm11.53  1988  19.36vOLD  1989  19.36aivOLD  1990  19.12vv  1991  eeanv  1993  eeeanv  1994  spimv  2014  spimev  2015  chvarv  2019  cbvalv  2028  cbvexv  2029  cbvald  2030  cbval2  2032  cbval2v  2034  cbvex2v  2035  cbvaldva  2036  cbvexdva  2037  axc9lem2  2044  axc16i  2068  dvelimnf  2085  cleljustALT  2112  sbiedv  2154  equsb3lem  2177  equsb3  2178  equsb3ALT  2179  elsb3  2180  elsb4  2181  sbhb  2184  sbnf2  2185  sbcom2  2191  sbcom4  2192  dfsb7  2201  sbid2v  2203  sbel2x  2205  sbco4lem  2211  sbco4  2212  2sb8e  2213  exsb  2214  euf  2294  mo2  2295  nfeud2  2298  eubidv  2306  mobidv  2307  sb8eu  2319  sb8euOLD  2320  mo3OLD  2325  euexALT  2329  euorv  2331  sbmo  2333  mo4f  2334  mo4  2335  moanimv  2349  euanv  2352  mopickOLD  2354  moexexv  2361  2mo  2370  2moOLD  2371  2mos  2372  2eu4OLD  2378  2eu6  2380  2eu6OLD  2381  bm1.1  2437  bm1.1OLD  2438  cleqh  2569  eqsb3lem  2573  eqsb3  2574  clelsb3  2575  abbiOLD  2586  abbidv  2590  cbvabv  2597  clelab  2598  clelabOLD  2599  nfcjust  2603  nfcv  2616  nfeqd  2623  nfeld  2624  nfabd2  2637  dvelimdc  2639  cleqfOLD  2644  sbabel  2647  sbabelOLD  2648  r19.21vOLD  2860  ralimdvaOLD  2863  ralrimivOLD  2867  ralrimdvOLD  2871  ralbidvaOLD  2891  ralbidvOLD  2894  2ralbida  2895  2ralbidvaOLD  2897  reximdvaiOLD  2927  r19.23vOLD  2935  rexlimivOLD  2941  rexlimdvOLD  2945  rexbidvaALT  2963  rexbidvALT  2966  r19.29af  2994  r19.29an  2995  r19.29a  2996  r19.37v  3004  reean  3021  reeanv  3022  reubidva  3038  rmobidva  3043  cbvralf  3075  cbvreu  3079  cbvralv  3081  cbvrexv  3082  cbvreuv  3083  cbvrmov  3084  cbvralsv  3092  cbvrexsv  3093  sbralie  3094  cbvrab  3104  cbvrabv  3105  issetf  3111  ceqsalv  3134  ceqsralv  3135  ceqsexv  3143  ceqsex2  3144  ceqsex2v  3145  vtocld  3156  vtocl  3158  vtoclg  3164  vtocl2g  3168  vtoclga  3170  vtocl2gaf  3171  vtocl2ga  3172  vtocl3gaf  3173  vtocl3ga  3174  spcimdv  3188  spcgv  3191  spcegv  3192  rspct  3200  rspc  3201  rspce  3202  rspcv  3203  rspcev  3207  rspc2v  3216  eqvincf  3224  ceqsexgv  3229  elabgt  3240  elab  3243  elabg  3244  elab3g  3249  elrab3t  3253  elrab  3254  ralab2  3261  rexab2  3263  mob2  3276  mob  3278  reu2  3284  reu2eqd  3293  nfcdeq  3321  sbcco  3347  sbcco2  3348  cbvsbcv  3354  sbcieg  3357  sbcie2g  3358  sbcied  3361  elrabsf  3363  sbcbidv  3379  sbcg  3390  sbc2iegf  3391  sbc2ie  3392  rmo2  3413  rmo3  3415  nfcsb1d  3434  nfcsbd  3437  csbiebt  3440  csbied  3447  csbie2t  3449  cbvralcsf  3452  cbvreucsf  3454  cbvrabcsf  3455  cbvralv2  3456  cbvrexv2  3457  dfss2f  3480  uniiunlem  3574  rspn0  3796  csbeq2dv  3831  sbcnestg  3836  sbnfc2  3846  sbss  3927  nfifd  3957  rabsnifsb  4084  euabsn  4088  nfuni  4241  nfunid  4242  eluniab  4246  nfint  4281  elintab  4282  rabasiun  4319  iineq2dv  4338  disjiun  4430  disjxun  4437  opabbidv  4502  nfopab  4504  cbvopab  4507  cbvopabv  4508  cbvopab1  4509  cbvopab2  4510  cbvopab1s  4511  cbvopab1v  4512  mpteq12f  4515  mpteq2dva  4525  cbvmpt  4529  axrep1  4551  axrep2  4552  axrep3  4553  axrep4  4554  axrep5  4555  zfrepclf  4556  axsep  4559  zfnuleu  4565  reusv2lem2  4639  reusv2lem3  4640  reusv2lem4  4641  reusv2  4643  reusv3  4645  reusv6OLD  4648  alxfr  4650  ralxfrALT  4656  copsex2t  4723  copsex2g  4724  opelopabaf  4760  nfso  4795  pofun  4805  nffr  4842  opeliunxp  5040  opeliunxp2  5130  ralxpf  5138  dfdmf  5185  dfrnf  5230  elrnmpt1  5240  asymref2  5372  intirr  5373  nfiotad  5537  cbviota  5539  cbviotav  5540  sb8iota  5541  iota2d  5559  iota2  5560  dffun6f  5584  fun11  5635  imadif  5645  funimaexg  5647  isarep1  5649  isarep2  5650  fv3  5861  tz6.12f  5866  tz6.12c  5867  opabiotafun  5909  funfv2f  5917  fvmptdf  5943  fvmptdv  5944  fvmptt  5947  fvopab5  5955  eqfnfv2f  5961  ralrnmpt  6016  f1ompt  6029  ffnfv  6033  ffnfvf  6034  fmptco  6040  elabrex  6130  dff13f  6142  fliftfun  6185  cbvriota  6242  cbvriotav  6243  riota2  6254  riota5f  6256  oprabv  6318  nfoprab  6322  oprabbidv  6324  mpt2eq123  6329  cbvoprab1  6342  cbvoprab2  6343  cbvoprab12  6344  cbvoprab12v  6345  cbvoprab3  6346  cbvoprab3v  6347  cbvmpt2x  6348  ralrnmpt2  6390  ovmpt2dx  6402  ovmpt2df  6407  ovmpt2dv  6408  ov3  6412  ovmpt3rab1  6507  ofrfval2  6530  onminex  6615  tfis  6662  tfis2  6664  tfisi  6666  tfinds  6667  tfindes  6670  peano5  6696  findes  6703  fun11iun  6733  abrexex2g  6750  opabex3d  6751  opabex3  6752  abrexex2  6754  dfoprab4f  6831  fmpt2x  6839  offval22  6852  ovmptss  6854  tposoprab  6983  fvmpt2curryd  6992  nfrecs  7036  tfr3  7060  nfrdg  7072  tz7.48-1  7100  tz7.49  7102  eqerlem  7335  erovlem  7399  mptelixpg  7499  boxcutc  7505  dom2lem  7548  xpf1o  7672  mapxpen  7676  nneneq  7693  pssnn  7731  findcard2  7752  ac6sfi  7756  fiint  7789  indexfi  7820  wdom2d  7998  ixpiunwdom  8009  cantnflem1  8099  r1val1  8195  rankuni2b  8262  scottexs  8296  scott0s  8297  dfac8clem  8404  acni2  8418  aceq1  8489  dfac5lem5  8499  kmlem15  8535  infpssrlem4  8677  fin23lem27  8699  hsmexlem2  8798  hsmexlem4  8800  axcc3  8809  domtriomlem  8813  axdc3lem2  8822  axdc3lem4  8824  axdc4lem  8826  ac6num  8850  ac6c4  8852  zorn2lem4  8870  zorn2lem5  8871  iunfo  8905  iundom2g  8906  uniimadomf  8911  konigthlem  8934  axrepndlem2  8959  axunnd  8962  axpowndlem2  8964  axpowndlem4  8966  axregndlem2  8969  axacndlem5  8978  zfcndrep  8981  zfcndinf  8985  pwfseqlem4a  9028  pwfseqlem4  9029  tskuni  9150  gruiin  9177  reclem2pr  9415  dedekind  9733  dedekindle  9734  fimaxre3  10487  uzindOLD  10953  nn0ind-raph  10960  uzind4s  11142  nnwof  11149  lbzbi  11171  fzrevral  11767  rabssnn0fi  12077  fsuppmapnn0fiublem  12078  fsuppmapnn0fiub  12079  fsuppmapnn0fiubex  12080  seqof2  12147  cotr2g  12894  trclfvcotr  12927  rlim2  13401  ello1mpt  13426  climeu  13460  o1compt  13492  summolem2a  13619  zsum  13622  sumss  13628  sumss2  13630  fsumcvg2  13631  fsum2dlem  13667  fsum00  13694  o1fsum  13709  nfcprod1  13799  nfcprod  13800  prodmolem2a  13823  zprod  13826  fprod  13830  fprodntriv  13831  prodss  13836  fprodn0  13865  fprod2dlem  13866  prmind2  14312  iserodd  14443  pcmpt  14495  pcmptdvds  14497  mreexexd  15137  catpropd  15197  invfuc  15462  natpropd  15464  fucpropd  15465  initoeu2  15494  acsmapd  16007  gsumsnd  17175  gsumsnf  17176  gsumunsnfd  17179  gsummptf1o  17186  gsummpt1n0  17188  gsum2d2lem  17197  gsumcom2  17199  gsummptnn0fz  17209  gsummptnn0fzv  17210  dprdwdOLD2  17240  dprdwdOLD  17246  dprd2d2  17288  gsummoncoe1  18541  gsumply1eq  18542  mdetralt2  19278  mdetunilem2  19282  madugsum  19312  gsummatr01lem4  19327  cpmatmcllem  19386  pmatcollpwfi  19450  cayleyhamilton1  19560  neiptopnei  19800  neiptopreu  19801  neitr  19848  fiuncmp  20071  iunconlem  20094  iuncon  20095  2ndcdisj  20123  dissnlocfin  20196  elptr2  20241  ptbasfi  20248  ptcld  20280  ptcldmpt  20281  ptclsg  20282  ptcnplem  20288  ptcnp  20289  cnmpt11  20330  cnmpt21  20338  cnmptcom  20345  imasnopn  20357  imasncld  20358  imasncls  20359  xkocnv  20481  elmptrab  20494  isfildlem  20524  alexsubALTlem3  20715  cnextfvval  20731  utopsnneiplem  20916  isucn2  20948  cfilucfilOLD  21238  cfilucfil  21239  blval2  21244  restmetu  21256  ovoliunlem3  22081  ovoliun  22082  ovoliun2  22083  ovoliunnul  22084  finiunmbl  22120  volfiniun  22123  iundisj  22124  iunmbl  22129  voliun  22130  iunmbl2  22133  mbfeqalem  22215  mbfsup  22237  mbfinf  22238  mbflim  22241  itg2splitlem  22321  itg2split  22322  isibl2  22339  cbvitg  22348  itgeqa  22386  itgss3  22387  itgfsum  22399  itgabs  22407  itggt0  22414  itgcn  22415  limcmpt  22453  limciun  22464  dvmptfsum  22542  dvlipcn  22561  dvfsumlem2  22594  dvfsumlem4  22596  dvfsumrlim  22598  dvfsum2  22601  itgsubst  22616  coeeq2  22805  dgrle  22806  ulmss  22958  leibpi  23470  rlimcnp  23493  rlimcnp2  23494  o1cxp  23502  fsumdvdscom  23659  lgseisenlem2  23823  dchrisumlema  23871  dchrisumlem2  23873  dchrisumlem3  23874  istrkg2ld  24056  mptelee  24400  ex-natded9.26  25342  isch3  26357  atom1d  27470  chirred  27512  spc2ed  27570  19.9d2r  27576  clelsb3f  27577  mo5f  27581  rmoeq  27584  rmo4fOLD  27593  rmo4f  27594  foresf1o  27602  elabreximdv  27608  rabss3d  27611  iuninc  27638  cbvdisjf  27644  disjorf  27650  disjabrex  27653  iundisjf  27659  disjunsn  27664  dfrel4  27668  brabgaf  27676  elsnxp  27684  ac6sf2  27687  dfimafnf  27694  suppss2f  27698  fimarab  27704  cbvmptf  27715  mpteq12df  27718  feqmptdf  27723  fmptcof2  27724  acunirnmpt2  27727  acunirnmpt2f  27728  aciunf1lem  27729  aciunf1  27730  ofpreima  27734  funcnvmptOLD  27736  funcnv5mpt  27738  funcnv4mpt  27739  padct  27776  cnvoprab  27777  f1od2  27778  fpwrelmap  27787  xrofsup  27816  iundisjfi  27835  nnindf  27844  nn0min  27845  2sqmo  27871  gsummpt2d  28006  isarchiofld  28042  reff  28077  locfinreflem  28078  cmpcref  28088  ordtconlem1  28141  qqhval2  28197  esumeq12dva  28261  esumeq2dv  28267  esumrnmpt  28281  esumpad  28284  esumpad2  28285  esumadd  28286  gsumesum  28288  esumlub  28289  esumsnf  28293  esumpr  28295  esumrnmpt2  28297  esumfzf  28298  esumfsup  28299  esumpcvgval  28307  esumpmono  28308  esumcocn  28309  hasheuni  28314  esumcvg  28315  esumgect  28319  esum2dlem  28321  esum2d  28322  esumiun  28323  sigapildsyslem  28387  sigapildsys  28388  measvunilem  28420  measvunilem0  28421  measvuni  28422  measiuns  28425  measiun  28426  measinblem  28428  voliune  28438  volfiniune  28439  volmeas  28440  ddemeas  28445  oms0  28505  omssubadd  28508  carsgclctunlem1  28525  carsggect  28526  omsmeas  28531  eulerpartlemgvv  28579  dstrvprob  28674  ballotlemodife  28700  lgamgulmlem2  28836  lgamgulmlem6  28840  cvmcov  28972  untsucf  29323  mpteq12d  29442  setinds2  29452  dfon2lem1  29455  dfon2lem3  29457  wfisg  29529  wfis2g  29533  trpredmintr  29554  frinsg  29565  frins2g  29569  frins2  29570  nfwrecs  29578  wl-equsb3  30244  wl-sb8eut  30262  ptrest  30288  heicant  30289  mbfposadd  30302  itgabsnc  30324  itggt0cn  30327  ftc1anclem5  30334  finminlem  30376  upixp  30460  indexa  30464  indexdom  30465  filbcmb  30471  sdclem2  30475  sdclem1  30476  fdc1  30479  totbndbnd  30525  sbcalf  30757  sbcexf  30758  scottexf  30816  scott0f  30817  prtlem5  30837  mzpexpmpt  30917  eq0rabdioph  30949  rexrabdioph  30967  rexfrabdioph  30968  elnn0rabdioph  30976  dvdsrabdioph  30983  fphpd  30989  monotuz  31116  monotoddzz  31118  oddcomabszz  31119  setindtr  31205  dford4  31210  wdom2d2  31216  aomclem6  31244  aomclem8  31246  flcidc  31364  areaquad  31425  binomcxplemdvsum  31501  binomcxplemnotnn0  31502  aaanv  31535  pm11.57  31536  pm11.58  31537  pm11.59  31538  pm11.71  31544  pm13.192  31558  pm14.12  31569  evth2f  31630  elunif  31631  fvelrnbf  31633  evthf  31642  fnchoice  31644  sumpair  31650  rfcnnnub  31651  refsum2cn  31653  elabrexg  31670  suprnmpt  31691  upbdrech  31744  ssfiunibd  31748  iccshift  31797  iooshift  31801  fsumclf  31806  fsumsplitf  31807  fsummulc1f  31808  fsumnncl  31811  fsumsplit1  31812  fmul01  31813  fmuldfeqlem1  31815  fmuldfeq  31816  fmul01lt1lem1  31817  fmul01lt1lem2  31818  fmul01lt1  31819  infrglb  31823  fprodsplitf  31828  fprodsplit1f  31832  fprodsplit1  31838  fprodexp  31839  fprodabs2  31841  fprodle  31843  mccllem  31844  mccl  31845  climexp  31850  climsuse  31853  climrecf  31854  climinff  31856  climaddf  31860  mullimc  31861  ellimcabssub0  31862  islptre  31864  climf  31867  mullimcf  31868  rexlim2d  31870  idlimc  31871  limcperiod  31873  limcrecl  31874  sumnnodd  31875  islpcn  31884  limsupre  31886  limcleqr  31889  neglimc  31892  addlimc  31893  0ellimcdiv  31894  limclner  31896  cncfshift  31915  icccncfext  31929  cncficcgt0  31930  cncfiooicclem1  31935  cncfiooicc  31936  cncfioobd  31939  fprodcncf  31943  dvmptmulf  31973  dvnmptdivc  31974  dvnmul  31979  dvmptfprodlem  31980  dvmptfprod  31981  dvnprodlem1  31982  dvnprodlem2  31983  iblsplitf  32008  iblspltprt  32011  itgioocnicc  32015  iblcncfioo  32016  itgspltprt  32017  itgperiod  32019  stoweidlem3  32024  stoweidlem14  32035  stoweidlem17  32038  stoweidlem19  32040  stoweidlem20  32041  stoweidlem26  32047  stoweidlem27  32048  stoweidlem28  32049  stoweidlem29  32050  stoweidlem31  32052  stoweidlem34  32055  stoweidlem35  32056  stoweidlem36  32057  stoweidlem39  32060  stoweidlem42  32063  stoweidlem43  32064  stoweidlem44  32065  stoweidlem46  32067  stoweidlem48  32069  stoweidlem49  32070  stoweidlem50  32071  stoweidlem51  32072  stoweidlem52  32073  stoweidlem53  32074  stoweidlem54  32075  stoweidlem56  32077  stoweidlem57  32078  stoweidlem59  32080  stoweidlem60  32081  stoweidlem61  32082  stoweidlem62  32083  stoweid  32084  wallispilem3  32088  stirlinglem13  32107  stirling  32110  fourierdlem16  32144  fourierdlem21  32149  fourierdlem22  32150  fourierdlem31  32159  fourierdlem39  32167  fourierdlem48  32176  fourierdlem51  32179  fourierdlem53  32181  fourierdlem68  32196  fourierdlem69  32197  fourierdlem71  32199  fourierdlem73  32201  fourierdlem77  32205  fourierdlem80  32208  fourierdlem81  32209  fourierdlem82  32210  fourierdlem83  32211  fourierdlem86  32214  fourierdlem87  32215  fourierdlem89  32217  fourierdlem91  32219  fourierdlem93  32221  fourierdlem94  32222  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  fourierdlem113  32241  elaa2  32256  etransclem18  32274  etransclem22  32278  etransclem23  32279  etransclem32  32288  etransclem35  32291  etransclem44  32300  etransclem46  32302  etransclem48  32304  rexsb  32412  rmoanim  32423  2reu4a  32433  ffnafv  32495  2zrngagrp  33003  2zrngmmgm  33006  opeliun2xp  33176  cbvmpt2x2  33179  ovmpt2rdx  33183  aacllem  33604  ssralv2  33688  tratrb  33697  iunconlem2  34136  bnj919  34226  bnj1146  34251  bnj1379  34290  bnj1385  34292  bnj1400  34295  bnj1476  34306  bnj1534  34312  bnj1542  34316  bnj110  34317  bnj121  34329  bnj124  34330  bnj130  34333  bnj207  34340  bnj571  34365  bnj605  34366  bnj580  34372  bnj607  34375  bnj611  34377  bnj873  34383  bnj849  34384  bnj900  34388  bnj916  34392  bnj1000  34400  bnj964  34402  bnj981  34409  bnj985  34412  bnj1014  34419  bnj1123  34443  bnj1128  34447  bnj1228  34468  bnj1204  34469  bnj1279  34475  bnj1307  34480  bnj1321  34484  bnj1388  34490  bnj1398  34491  bnj1408  34493  bnj1417  34498  bnj1444  34500  bnj1445  34501  bnj1446  34502  bnj1449  34505  bnj1467  34511  bnj1489  34513  bnj1312  34515  bnj1497  34517  bnj1518  34521  bnj1525  34526  bnj1529  34527  bj-nexdvt  34652  bj-spimvv  34683  bj-spimevv  34684  bj-chvarvv  34688  bj-cbv3v2  34690  bj-cbvalvv  34699  bj-cbvexvv  34700  bj-cbvaldv  34701  bj-cbval2v  34703  bj-cbval2vv  34705  bj-cbvex2vv  34706  bj-cbvaldvav  34707  bj-cbvexdvav  34708  bj-drnf2v  34730  bj-abbi  34762  bj-abbidv  34766  bj-axrep1  34775  bj-axrep2  34776  bj-axrep3  34777  bj-axrep4  34778  bj-axrep5  34779  bj-axsep  34780  ax11-pm2  34810  bj-clelsb3  34825  bj-nfcjust  34827  bj-ceqsalv  34860  bj-vtocl  34882  bj-inrab2  34897  fsumshftd  35079  fsumshftdOLD  35080  riotasv2d  35085  riotasv2s  35086  riotasv3d  35088  glbconxN  35499  pmapglbx  35890  pmapglb2xN  35893  cdleme26ee  36483  cdleme31sn  36503  cdleme31sn1  36504  cdlemefr29exN  36525  cdlemefs32sn1aw  36537  cdleme43fsv1snlem  36543  cdleme41sn3a  36556  cdleme32fva  36560  cdleme32d  36567  cdleme32f  36569  cdleme40m  36590  cdleme40n  36591  cdleme42b  36601  cdlemk36  37036  cdlemk38  37038  cdlemkid  37059  cdlemk19x  37066  cdlemk11t  37069  dihvalcqpre  37359  mapdheq  37852  hdmap1eq  37926  hdmapval2lem  37958  frege70  38411  frege72  38413
  Copyright terms: Public domain W3C validator