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

Theorem nfv 1626
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-17 1623 . 2  |-  ( ph  ->  A. x ph )
21nfi 1557 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1550
This theorem is referenced by:  nfvd  1627  dvelimhw  1872  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  1933  eeeanv  1934  nexdv  1937  spimv  1961  spimev  1962  ax12olem4  1975  cbvalv  2052  cbvexv  2053  cbval2  2054  cbvex2  2055  cbval2v  2056  cbvex2v  2057  cbvaldva  2060  cbvexdva  2061  cleljustALT  2065  dvelimnf  2067  sbiedv  2086  ax16i  2095  ax16ALT2  2097  equsb3lem  2150  equsb3  2151  elsb3  2152  elsb4  2153  sbhb  2156  sbnf2  2157  pm11.07  2164  dfsb7  2171  sbid2v  2173  exsb  2180  exsbOLD  2181  euf  2260  eubidv  2262  nfeud2  2266  sb8eu  2272  mo  2276  euex  2277  euorv  2282  sbmo  2284  mo4f  2286  mo4  2287  mobidv  2289  eu5  2292  moim  2300  morimv  2302  moanim  2310  moanimv  2312  euanv  2315  mopick  2316  moexexv  2324  2mo  2332  2mos  2333  2eu4  2337  2eu6  2339  bm1.1  2389  eqsb3lem  2504  eqsb3  2505  clelsb3  2506  abbi  2514  abbidv  2518  cbvabv  2523  clelab  2524  nfcjust  2528  nfcv  2540  nfeqd  2554  nfeld  2555  nfabd2  2558  dvelimdc  2560  cleqf  2564  sbabel  2566  ralbidva  2682  rexbidva  2683  ralbidv  2686  rexbidv  2687  2ralbida  2705  2ralbidva  2706  ralimdva  2744  ralrimiv  2748  r19.21v  2753  ralrimdv  2755  reximdvai  2776  r19.23v  2782  rexlimiv  2784  rexlimdv  2789  r19.29af  2809  r19.29a  2810  r19.37av  2818  r19.41v  2821  reean  2834  reeanv  2835  reubidva  2851  rmobidva  2856  cbvralf  2886  cbvreu  2890  cbvralv  2892  cbvrexv  2893  cbvreuv  2894  cbvrmov  2895  cbvralsv  2903  cbvrexsv  2904  sbralie  2905  cbvrab  2914  cbvrabv  2915  issetf  2921  ceqsalv  2942  ceqsralv  2943  ceqsexv  2951  ceqsex2  2952  ceqsex2v  2953  vtocld  2964  vtocl  2966  vtoclg  2971  vtocl2g  2975  vtoclga  2977  vtocl2gaf  2978  vtocl2ga  2979  vtocl3gaf  2980  vtocl3ga  2981  spcimdv  2993  spcgv  2996  spcegv  2997  rspct  3005  rspc  3006  rspce  3007  rspcv  3008  rspcev  3012  rspc2v  3018  eqvincf  3024  ceqsexgv  3028  elabgt  3039  elab  3042  elabg  3043  elab3g  3048  elrab  3052  ralab2  3059  rexab2  3061  eqeu  3065  mo2icl  3073  mob2  3074  mob  3076  reu2  3082  reu3  3084  nfcdeq  3118  sbcco  3143  sbcco2  3144  cbvsbcv  3150  sbcieg  3153  sbcie2g  3154  sbcied  3157  elrabsf  3159  sbcbidv  3175  sbcg  3186  sbc2iegf  3187  sbc2ie  3188  rmo2  3206  rmo3  3208  csbeq2dv  3236  nfcsb1d  3241  nfcsbd  3244  csbiebt  3247  csbied  3253  csbie2t  3255  sbcnestg  3260  sbnfc2  3269  cbvralcsf  3271  cbvreucsf  3273  cbvrabcsf  3274  cbvralv2  3275  cbvrexv2  3276  dfss2f  3299  uniiunlem  3391  sbss  3697  nfifd  3722  euabsn  3836  nfuni  3981  nfunid  3982  eluniab  3987  nfint  4020  elintab  4021  iineq2dv  4075  disjiun  4162  disjxun  4170  opabbidv  4231  nfopab  4233  cbvopab  4236  cbvopabv  4237  cbvopab1  4238  cbvopab2  4239  cbvopab1s  4240  cbvopab1v  4241  mpteq12f  4245  mpteq2dva  4255  cbvmpt  4259  axrep1  4281  axrep2  4282  axrep3  4283  axrep4  4284  axrep5  4285  zfrepclf  4286  axsep  4289  zfnuleu  4295  eunex  4352  moabex  4382  copsex2t  4403  copsex2g  4404  opelopabaf  4438  nfso  4469  pofun  4479  nffr  4516  reusv2lem2  4684  reusv2lem3  4685  reusv2lem4  4686  reusv2  4688  reusv3  4690  reusv6OLD  4693  alxfr  4695  ralxfrALT  4701  onminex  4746  tfis  4793  tfis2  4795  tfisi  4797  tfinds  4798  tfindes  4801  peano5  4827  findes  4834  opeliunxp  4888  opeliunxp2  4972  ralxpf  4978  dfdmf  5023  dfrnf  5067  elrnmpt1  5078  asymref2  5210  intirr  5211  nfiotad  5380  cbviota  5382  cbviotav  5383  sb8iota  5384  iota2d  5402  iota2  5403  dffun3  5424  dffun6f  5427  fun11  5475  imadif  5487  funimaexg  5489  isarep1  5491  isarep2  5492  fun11iun  5654  fv3  5703  tz6.12f  5708  tz6.12c  5709  funfv2f  5751  fvmptdf  5775  fvmptdv  5776  fvmptt  5779  eqfnfv2f  5790  ralrnmpt  5837  f1ompt  5850  ffnfv  5853  ffnfvf  5854  fmptco  5860  elabrex  5944  abrexex2g  5947  opabex3d  5948  opabex3  5949  abrexex2  5960  dff13f  5965  fliftfun  5993  nfoprab  6085  oprabbidv  6087  mpt2eq123  6092  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvoprab12v  6106  cbvoprab3  6107  cbvoprab3v  6108  cbvmpt2x  6109  ralrnmpt2  6143  ovmpt2dx  6159  ovmpt2df  6164  ovmpt2dv  6165  ov3  6169  ofrfval2  6282  dfoprab4f  6364  fmpt2x  6376  ovmptss  6387  tposoprab  6474  fvopab5  6493  opabiotafun  6495  cbvriota  6519  cbvriotav  6520  riota2  6531  riota5f  6533  riotasv2d  6553  riotasv2dOLD  6554  riotasv2s  6555  riotasv3d  6557  nfrecs  6594  tfrlem1  6595  tfr3  6619  nfrdg  6631  tz7.48-1  6659  tz7.49  6661  eqerlem  6896  erovlem  6959  mptelixpg  7058  boxcutc  7064  dom2lem  7106  xpf1o  7228  mapxpen  7232  nneneq  7249  pssnn  7286  findcard2  7307  ac6sfi  7310  fiint  7342  indexfi  7372  wdom2d  7504  ixpiunwdom  7515  sucprcreg  7523  r1val1  7668  rankuni2b  7735  scottexs  7767  scott0s  7768  dfac8clem  7869  acni2  7883  aceq1  7954  dfac5lem5  7964  kmlem15  8000  infpssrlem4  8142  fin23lem27  8164  hsmexlem2  8263  hsmexlem4  8265  axcc3  8274  domtriomlem  8278  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  ac6num  8315  ac6c4  8317  zorn2lem4  8335  zorn2lem5  8336  iunfo  8370  iundom2g  8371  uniimadomf  8376  konigthlem  8399  axrepndlem2  8424  axunnd  8427  axpowndlem2  8429  axpowndlem4  8431  axregndlem2  8434  axacndlem5  8442  zfcndrep  8445  zfcndpow  8447  zfcndinf  8449  zfcndac  8450  pwfseqlem4a  8492  pwfseqlem4  8493  tskuni  8614  gruiin  8641  grothprim  8665  reclem2pr  8881  fimaxre3  9913  uzindOLD  10320  nn0ind-raph  10326  uzind4s  10492  nnwof  10499  lbzbi  10520  fzrevral  11086  seqof2  11336  rlim2  12245  ello1mpt  12270  climeu  12304  o1compt  12336  summolem2a  12464  zsum  12467  fsum  12469  sumss  12473  sumss2  12475  fsumcvg2  12476  fsum2dlem  12509  fsum00  12532  o1fsum  12547  prmind2  13045  iserodd  13164  pcmpt  13216  pcmptdvds  13218  mreexexd  13828  catpropd  13890  invfuc  14126  natpropd  14128  fucpropd  14129  acsmapd  14559  gsum2d2lem  15502  gsumcom2  15504  dprdwd  15524  dprd2d2  15557  neiptopnei  17151  neiptopreu  17152  neitr  17198  fiuncmp  17421  iunconlem  17443  iuncon  17444  2ndcdisj  17472  elptr2  17559  ptbasfi  17566  ptcld  17598  ptcldmpt  17599  ptclsg  17600  ptcnplem  17606  ptcnp  17607  cnmpt11  17648  cnmpt21  17656  cnmptcom  17663  imasnopn  17675  imasncld  17676  imasncls  17677  xkocnv  17799  elmptrab  17812  isfildlem  17842  alexsubALTlem3  18033  cnextfvval  18049  utopsnneiplem  18230  isucn2  18262  cfilucfilOLD  18552  cfilucfil  18553  blval2  18558  restmetu  18570  ovoliunlem3  19353  ovoliun  19354  ovoliun2  19355  ovoliunnul  19356  finiunmbl  19391  volfiniun  19394  iundisj  19395  iunmbl  19400  voliun  19401  iunmbl2  19404  mbfeqalem  19487  mbfsup  19509  mbfinf  19510  mbflim  19513  itg2splitlem  19593  itg2split  19594  isibl2  19611  cbvitg  19620  itgeqa  19658  itgss3  19659  itgfsum  19671  itgabs  19679  itggt0  19686  itgcn  19687  limcmpt  19723  limciun  19734  dvmptfsum  19812  dvlipcn  19831  dvfsumlem2  19864  dvfsumlem4  19866  dvfsumrlim  19868  dvfsum2  19871  itgsubst  19886  coeeq2  20114  dgrle  20115  ulmss  20266  leibpi  20735  rlimcnp  20757  rlimcnp2  20758  o1cxp  20766  fsumdvdscom  20923  lgseisenlem2  21087  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  ex-natded9.26  21680  isch3  22697  atom1d  23809  chirred  23851  19.9d2r  23922  clelsb3f  23924  mo5f  23925  rmo4fOLD  23936  rmo4f  23937  elabreximdv  23945  rabss3d  23948  iuninc  23964  cbvdisjf  23968  disjorf  23974  disjabrex  23977  iundisjf  23982  dfrel4  23987  dfimafnf  23996  suppss2f  24002  cbvmptf  24021  feqmptdf  24028  fmptcof2  24029  ofpreima  24034  funcnvmptOLD  24035  funcnv5mpt  24037  funcnv4mpt  24038  xrofsup  24079  iundisjfi  24105  qqhval2  24319  esumeq12dva  24382  esumeq2dv  24388  esumc  24399  esumadd  24401  gsumesum  24404  esumlub  24405  esumpr  24410  esumfzf  24412  esumfsup  24413  esumpcvgval  24421  esumpmono  24422  esumcocn  24423  hasheuni  24428  esumcvg  24429  measvunilem  24519  measvunilem0  24520  measvuni  24521  measiuns  24524  measiun  24525  measinblem  24527  voliune  24538  volfiniune  24539  volmeas  24540  dstrvprob  24682  ballotlemodife  24708  lgamgulmlem2  24767  lgamgulmlem6  24771  cvmcov  24903  untsucf  25112  dedekind  25140  dedekindle  25141  nfcprod1  25189  nfcprod  25190  prodmolem2a  25213  zprod  25216  fprod  25220  fprodntriv  25221  prodss  25226  fprodn0  25256  fprod2dlem  25257  mpteq12d  25342  setinds2  25350  dfon2lem1  25353  dfon2lem3  25355  wfisg  25423  wfis2g  25427  trpredmintr  25448  frinsg  25459  frins2g  25463  frins2  25464  wfr3g  25469  frr3g  25494  mptelee  25738  itgabsnc  26173  itggt0cn  26176  finminlem  26211  upixp  26321  indexa  26325  indexdom  26326  filbcmb  26332  sdclem2  26336  sdclem1  26337  fdc1  26340  totbndbnd  26388  prtlem5  26595  mzpexpmpt  26692  eq0rabdioph  26725  rexrabdioph  26744  rexfrabdioph  26745  elnn0rabdioph  26753  dvdsrabdioph  26760  fphpd  26767  monotuz  26894  monotoddzz  26896  oddcomabszz  26897  setindtr  26985  dford4  26990  wdom2d2  26996  aomclem6  27024  aomclem8  27027  flcidc  27247  pm10.12  27421  19.31vv  27450  aaanv  27455  pm11.57  27456  pm11.58  27457  pm11.59  27458  pm11.71  27464  ax10ext  27474  pm13.192  27478  pm14.12  27489  evth2f  27553  elunif  27554  fvelrnbf  27556  evthf  27565  fnchoice  27567  sumpair  27573  rfcnnnub  27574  refsum2cn  27576  fmul01  27577  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  fmul01lt1  27583  infrglb  27589  climexp  27598  climsuse  27601  climrecf  27602  climinff  27604  stoweidlem3  27619  stoweidlem14  27630  stoweidlem17  27633  stoweidlem19  27635  stoweidlem20  27636  stoweidlem26  27642  stoweidlem27  27643  stoweidlem28  27644  stoweidlem29  27645  stoweidlem31  27647  stoweidlem34  27650  stoweidlem35  27651  stoweidlem36  27652  stoweidlem39  27655  stoweidlem42  27658  stoweidlem43  27659  stoweidlem44  27660  stoweidlem46  27662  stoweidlem48  27664  stoweidlem49  27665  stoweidlem50  27666  stoweidlem51  27667  stoweidlem52  27668  stoweidlem53  27669  stoweidlem54  27670  stoweidlem56  27672  stoweidlem57  27673  stoweidlem59  27675  stoweidlem60  27676  stoweidlem61  27677  stoweidlem62  27678  stoweid  27679  wallispilem3  27683  stirlinglem13  27702  stirling  27705  rexsb  27813  rmoanim  27824  2reu4a  27834  ffnafv  27902  ssralv2  28326  tratrb  28331  bnj919  28842  bnj1146  28868  bnj1379  28908  bnj1385  28910  bnj1400  28913  bnj1476  28924  bnj1534  28930  bnj1542  28934  bnj110  28935  bnj121  28947  bnj124  28948  bnj130  28951  bnj207  28958  bnj571  28983  bnj605  28984  bnj580  28990  bnj607  28993  bnj611  28995  bnj873  29001  bnj849  29002  bnj900  29006  bnj916  29010  bnj1000  29018  bnj964  29020  bnj981  29027  bnj985  29030  bnj1014  29037  bnj1123  29061  bnj1128  29065  bnj1228  29086  bnj1204  29087  bnj1279  29093  bnj1307  29098  bnj1321  29102  bnj1388  29108  bnj1398  29109  bnj1408  29111  bnj1417  29116  bnj1444  29118  bnj1445  29119  bnj1446  29120  bnj1449  29123  bnj1467  29129  bnj1489  29131  bnj1312  29133  bnj1497  29135  bnj1518  29139  bnj1525  29144  bnj1529  29145  spimvNEW7  29225  ax16iNEW7  29255  exsbNEW7  29300  exsbOLDNEW7  29301  equsb3lemNEW7  29302  equsb3NEW7  29303  elsb3NEW7  29304  elsb4NEW7  29305  sbhbwAUX7  29308  sbnf2NEW7  29309  sbid2vNEW7  29313  spimevNEW7  29325  sbiedvNEW7  29333  pm11.53OLD7  29384  19.12vvOLD7  29385  eeanvOLD7  29387  cbvalvOLD7  29412  cbvexvOLD7  29413  cbval2OLD7  29414  cbvex2OLD7  29415  cbval2vOLD7  29416  cbvex2vOLD7  29417  cbvaldvaOLD7  29420  cbvexdvaOLD7  29421  dvelimnfOLD7  29424  ax16ALT2OLD7  29427  sbhbOLD7  29444  dfsb7OLD7  29448  glbconxN  29860  pmapglbx  30251  pmapglb2xN  30254  cdleme26ee  30842  cdleme31sn  30862  cdleme31sn1  30863  cdlemefr29exN  30884  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme41sn3a  30915  cdleme32fva  30919  cdleme32d  30926  cdleme32f  30928  cdleme40m  30949  cdleme40n  30950  cdleme42b  30960  cdlemk36  31395  cdlemk38  31397  cdlemkid  31418  cdlemk19x  31425  cdlemk11t  31428  dihvalcqpre  31718  mapdheq  32211  hdmap1eq  32285  hdmapval2lem  32317
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-nf 1551
  Copyright terms: Public domain W3C validator