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

Theorem nfv 1630
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 1627 . 2  |-  ( ph  ->  A. x ph )
21nfi 1561 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1554
This theorem is referenced by:  nfvd  1631  dvelimhw  1877  19.21v  1914  19.23v  1915  pm11.53  1917  19.27v  1918  19.28v  1919  19.36v  1920  19.36aiv  1921  19.12vv  1922  19.37v  1923  19.41v  1925  19.42v  1929  eeanv  1938  eeeanv  1939  nexdv  1942  spimv  1964  spimev  1965  chvarv  1970  cbvalv  1985  cbvexv  1986  cbvald  1987  cbval2  1990  cbval2OLD  1991  cbvex2  1992  cbval2v  1993  cbvex2v  1994  cbvaldva  1995  cbvexdva  1996  ax12olem4  2009  ax16i  2052  dvelimnf  2076  cleljustALT  2106  sbiedv  2155  ax16ALT2  2157  equsb3lem  2179  equsb3  2180  elsb3  2181  elsb4  2182  sbhb  2185  sbnf2  2186  pm11.07  2193  dfsb7  2200  sbid2v  2202  exsb  2209  exsbOLD  2210  euf  2289  eubidv  2291  nfeud2  2295  sb8eu  2301  mo  2305  euex  2306  euorv  2311  sbmo  2313  mo4f  2315  mo4  2316  mobidv  2318  eu5  2321  moim  2329  morimv  2331  moanim  2339  moanimv  2341  euanv  2344  mopick  2345  moexexv  2353  2mo  2361  2mos  2362  2eu4  2366  2eu6  2368  bm1.1  2423  eqsb3lem  2538  eqsb3  2539  clelsb3  2540  abbi  2548  abbidv  2552  cbvabv  2557  clelab  2558  nfcjust  2562  nfcv  2574  nfeqd  2588  nfeld  2589  nfabd2  2592  dvelimdc  2594  cleqf  2598  sbabel  2600  ralbidva  2723  rexbidva  2724  ralbidv  2727  rexbidv  2728  2ralbida  2746  2ralbidva  2747  ralimdva  2786  ralrimiv  2790  r19.21v  2795  ralrimdv  2797  reximdvai  2818  r19.23v  2824  rexlimiv  2826  rexlimdv  2831  r19.29af  2851  r19.29a  2852  r19.37av  2860  r19.41v  2863  reean  2876  reeanv  2877  reubidva  2893  rmobidva  2898  cbvralf  2928  cbvreu  2932  cbvralv  2934  cbvrexv  2935  cbvreuv  2936  cbvrmov  2937  cbvralsv  2945  cbvrexsv  2946  sbralie  2947  cbvrab  2956  cbvrabv  2957  issetf  2963  ceqsalv  2984  ceqsralv  2985  ceqsexv  2993  ceqsex2  2994  ceqsex2v  2995  vtocld  3006  vtocl  3008  vtoclg  3013  vtocl2g  3017  vtoclga  3019  vtocl2gaf  3020  vtocl2ga  3021  vtocl3gaf  3022  vtocl3ga  3023  spcimdv  3035  spcgv  3038  spcegv  3039  rspct  3047  rspc  3048  rspce  3049  rspcv  3050  rspcev  3054  rspc2v  3060  eqvincf  3066  ceqsexgv  3070  elabgt  3081  elab  3084  elabg  3085  elab3g  3090  elrab  3094  ralab2  3101  rexab2  3103  eqeu  3107  mo2icl  3115  mob2  3116  mob  3118  reu2  3124  reu3  3126  nfcdeq  3160  sbcco  3185  sbcco2  3186  cbvsbcv  3192  sbcieg  3195  sbcie2g  3196  sbcied  3199  elrabsf  3201  sbcbidv  3217  sbcg  3228  sbc2iegf  3229  sbc2ie  3230  rmo2  3248  rmo3  3250  csbeq2dv  3278  nfcsb1d  3283  nfcsbd  3286  csbiebt  3289  csbied  3295  csbie2t  3297  sbcnestg  3302  sbnfc2  3311  cbvralcsf  3313  cbvreucsf  3315  cbvrabcsf  3316  cbvralv2  3317  cbvrexv2  3318  dfss2f  3341  uniiunlem  3433  sbss  3739  nfifd  3764  euabsn  3878  nfuni  4023  nfunid  4024  eluniab  4029  nfint  4062  elintab  4063  iineq2dv  4117  disjiun  4205  disjxun  4213  opabbidv  4274  nfopab  4276  cbvopab  4279  cbvopabv  4280  cbvopab1  4281  cbvopab2  4282  cbvopab1s  4283  cbvopab1v  4284  mpteq12f  4288  mpteq2dva  4298  cbvmpt  4302  axrep1  4324  axrep2  4325  axrep3  4326  axrep4  4327  axrep5  4328  zfrepclf  4329  axsep  4332  zfnuleu  4338  eunex  4395  moabex  4425  copsex2t  4446  copsex2g  4447  opelopabaf  4481  nfso  4512  pofun  4522  nffr  4559  reusv2lem2  4728  reusv2lem3  4729  reusv2lem4  4730  reusv2  4732  reusv3  4734  reusv6OLD  4737  alxfr  4739  ralxfrALT  4745  onminex  4790  tfis  4837  tfis2  4839  tfisi  4841  tfinds  4842  tfindes  4845  peano5  4871  findes  4878  opeliunxp  4932  opeliunxp2  5016  ralxpf  5022  dfdmf  5067  dfrnf  5111  elrnmpt1  5122  asymref2  5254  intirr  5255  nfiotad  5424  cbviota  5426  cbviotav  5427  sb8iota  5428  iota2d  5446  iota2  5447  dffun3  5468  dffun6f  5471  fun11  5519  imadif  5531  funimaexg  5533  isarep1  5535  isarep2  5536  fun11iun  5698  fv3  5747  tz6.12f  5752  tz6.12c  5753  funfv2f  5795  fvmptdf  5819  fvmptdv  5820  fvmptt  5823  eqfnfv2f  5834  ralrnmpt  5881  f1ompt  5894  ffnfv  5897  ffnfvf  5898  fmptco  5904  elabrex  5988  abrexex2g  5991  opabex3d  5992  opabex3  5993  abrexex2  6004  dff13f  6009  fliftfun  6037  nfoprab  6129  oprabbidv  6131  mpt2eq123  6136  cbvoprab1  6147  cbvoprab2  6148  cbvoprab12  6149  cbvoprab12v  6150  cbvoprab3  6151  cbvoprab3v  6152  cbvmpt2x  6153  ralrnmpt2  6187  ovmpt2dx  6203  ovmpt2df  6208  ovmpt2dv  6209  ov3  6213  ofrfval2  6326  dfoprab4f  6408  fmpt2x  6420  ovmptss  6431  tposoprab  6518  fvopab5  6537  opabiotafun  6539  cbvriota  6563  cbvriotav  6564  riota2  6575  riota5f  6577  riotasv2d  6597  riotasv2dOLD  6598  riotasv2s  6599  riotasv3d  6601  nfrecs  6638  tfrlem1  6639  tfr3  6663  nfrdg  6675  tz7.48-1  6703  tz7.49  6705  eqerlem  6940  erovlem  7003  mptelixpg  7102  boxcutc  7108  dom2lem  7150  xpf1o  7272  mapxpen  7276  nneneq  7293  pssnn  7330  findcard2  7351  ac6sfi  7354  fiint  7386  indexfi  7417  wdom2d  7551  ixpiunwdom  7562  sucprcreg  7570  r1val1  7715  rankuni2b  7782  scottexs  7816  scott0s  7817  dfac8clem  7918  acni2  7932  aceq1  8003  dfac5lem5  8013  kmlem15  8049  infpssrlem4  8191  fin23lem27  8213  hsmexlem2  8312  hsmexlem4  8314  axcc3  8323  domtriomlem  8327  axdc3lem2  8336  axdc3lem4  8338  axdc4lem  8340  ac6num  8364  ac6c4  8366  zorn2lem4  8384  zorn2lem5  8385  iunfo  8419  iundom2g  8420  uniimadomf  8425  konigthlem  8448  axrepndlem2  8473  axunnd  8476  axpowndlem2  8478  axpowndlem4  8480  axregndlem2  8483  axacndlem5  8491  zfcndrep  8494  zfcndpow  8496  zfcndinf  8498  zfcndac  8499  pwfseqlem4a  8541  pwfseqlem4  8542  tskuni  8663  gruiin  8690  grothprim  8714  reclem2pr  8930  fimaxre3  9962  uzindOLD  10369  nn0ind-raph  10375  uzind4s  10541  nnwof  10548  lbzbi  10569  fzrevral  11136  seqof2  11386  rlim2  12295  ello1mpt  12320  climeu  12354  o1compt  12386  summolem2a  12514  zsum  12517  fsum  12519  sumss  12523  sumss2  12525  fsumcvg2  12526  fsum2dlem  12559  fsum00  12582  o1fsum  12597  prmind2  13095  iserodd  13214  pcmpt  13266  pcmptdvds  13268  mreexexd  13878  catpropd  13940  invfuc  14176  natpropd  14178  fucpropd  14179  acsmapd  14609  gsum2d2lem  15552  gsumcom2  15554  dprdwd  15574  dprd2d2  15607  neiptopnei  17201  neiptopreu  17202  neitr  17249  fiuncmp  17472  bwth  17478  iunconlem  17495  iuncon  17496  2ndcdisj  17524  elptr2  17611  ptbasfi  17618  ptcld  17650  ptcldmpt  17651  ptclsg  17652  ptcnplem  17658  ptcnp  17659  cnmpt11  17700  cnmpt21  17708  cnmptcom  17715  imasnopn  17727  imasncld  17728  imasncls  17729  xkocnv  17851  elmptrab  17864  isfildlem  17894  alexsubALTlem3  18085  cnextfvval  18101  utopsnneiplem  18282  isucn2  18314  cfilucfilOLD  18604  cfilucfil  18605  blval2  18610  restmetu  18622  ovoliunlem3  19405  ovoliun  19406  ovoliun2  19407  ovoliunnul  19408  finiunmbl  19443  volfiniun  19446  iundisj  19447  iunmbl  19452  voliun  19453  iunmbl2  19456  mbfeqalem  19537  mbfsup  19559  mbfinf  19560  mbflim  19563  itg2splitlem  19643  itg2split  19644  isibl2  19661  cbvitg  19670  itgeqa  19708  itgss3  19709  itgfsum  19721  itgabs  19729  itggt0  19736  itgcn  19737  limcmpt  19775  limciun  19786  dvmptfsum  19864  dvlipcn  19883  dvfsumlem2  19916  dvfsumlem4  19918  dvfsumrlim  19920  dvfsum2  19923  itgsubst  19938  coeeq2  20166  dgrle  20167  ulmss  20318  leibpi  20787  rlimcnp  20809  rlimcnp2  20810  o1cxp  20818  fsumdvdscom  20975  lgseisenlem2  21139  dchrisumlema  21187  dchrisumlem2  21189  dchrisumlem3  21190  ex-natded9.26  21732  isch3  22749  atom1d  23861  chirred  23903  19.9d2r  23974  clelsb3f  23976  mo5f  23977  rmo4fOLD  23988  rmo4f  23989  elabreximdv  23997  rabss3d  24000  iuninc  24016  cbvdisjf  24020  disjorf  24026  disjabrex  24029  iundisjf  24034  dfrel4  24039  dfimafnf  24048  suppss2f  24054  cbvmptf  24073  feqmptdf  24080  fmptcof2  24081  ofpreima  24086  funcnvmptOLD  24087  funcnv5mpt  24089  funcnv4mpt  24090  xrofsup  24131  iundisjfi  24157  qqhval2  24371  esumeq12dva  24434  esumeq2dv  24440  esumc  24451  esumadd  24453  gsumesum  24456  esumlub  24457  esumpr  24462  esumfzf  24464  esumfsup  24465  esumpcvgval  24473  esumpmono  24474  esumcocn  24475  hasheuni  24480  esumcvg  24481  measvunilem  24571  measvunilem0  24572  measvuni  24573  measiuns  24576  measiun  24577  measinblem  24579  voliune  24590  volfiniune  24591  volmeas  24592  dstrvprob  24734  ballotlemodife  24760  lgamgulmlem2  24819  lgamgulmlem6  24823  cvmcov  24955  untsucf  25164  dedekind  25192  dedekindle  25193  nfcprod1  25241  nfcprod  25242  prodmolem2a  25265  zprod  25268  fprod  25272  fprodntriv  25273  prodss  25278  fprodn0  25308  fprod2dlem  25309  mpteq12d  25401  setinds2  25412  dfon2lem1  25415  dfon2lem3  25417  wfisg  25489  wfis2g  25493  trpredmintr  25514  frinsg  25525  frins2g  25529  frins2  25530  nfwrecs  25538  wfr3g  25542  frr3g  25586  mptelee  25839  heicant  26253  itgabsnc  26288  itggt0cn  26291  ftc1anclem5  26298  finminlem  26335  upixp  26445  indexa  26449  indexdom  26450  filbcmb  26456  sdclem2  26460  sdclem1  26461  fdc1  26464  totbndbnd  26512  prtlem5  26719  mzpexpmpt  26816  eq0rabdioph  26849  rexrabdioph  26868  rexfrabdioph  26869  elnn0rabdioph  26877  dvdsrabdioph  26884  fphpd  26891  monotuz  27018  monotoddzz  27020  oddcomabszz  27021  setindtr  27109  dford4  27114  wdom2d2  27120  aomclem6  27148  aomclem8  27150  flcidc  27370  pm10.12  27544  19.31vv  27573  aaanv  27578  pm11.57  27579  pm11.58  27580  pm11.59  27581  pm11.71  27587  ax10ext  27597  pm13.192  27601  pm14.12  27612  evth2f  27676  elunif  27677  fvelrnbf  27679  evthf  27688  fnchoice  27690  sumpair  27696  rfcnnnub  27697  refsum2cn  27699  fmul01  27700  fmuldfeqlem1  27702  fmuldfeq  27703  fmul01lt1lem1  27704  fmul01lt1lem2  27705  fmul01lt1  27706  infrglb  27712  climexp  27721  climsuse  27724  climrecf  27725  climinff  27727  stoweidlem3  27742  stoweidlem14  27753  stoweidlem17  27756  stoweidlem19  27758  stoweidlem20  27759  stoweidlem26  27765  stoweidlem27  27766  stoweidlem28  27767  stoweidlem29  27768  stoweidlem31  27770  stoweidlem34  27773  stoweidlem35  27774  stoweidlem36  27775  stoweidlem39  27778  stoweidlem42  27781  stoweidlem43  27782  stoweidlem44  27783  stoweidlem46  27785  stoweidlem48  27787  stoweidlem49  27788  stoweidlem50  27789  stoweidlem51  27790  stoweidlem52  27791  stoweidlem53  27792  stoweidlem54  27793  stoweidlem56  27795  stoweidlem57  27796  stoweidlem59  27798  stoweidlem60  27799  stoweidlem61  27800  stoweidlem62  27801  stoweid  27802  wallispilem3  27806  stirlinglem13  27825  stirling  27828  rexsb  27936  rmoanim  27947  2reu4a  27957  ffnafv  28025  oprabv  28103  ssralv2  28689  tratrb  28694  iunconlem2  29121  bnj919  29210  bnj1146  29236  bnj1379  29276  bnj1385  29278  bnj1400  29281  bnj1476  29292  bnj1534  29298  bnj1542  29302  bnj110  29303  bnj121  29315  bnj124  29316  bnj130  29319  bnj207  29326  bnj571  29351  bnj605  29352  bnj580  29358  bnj607  29361  bnj611  29363  bnj873  29369  bnj849  29370  bnj900  29374  bnj916  29378  bnj1000  29386  bnj964  29388  bnj981  29395  bnj985  29398  bnj1014  29405  bnj1123  29429  bnj1128  29433  bnj1228  29454  bnj1204  29455  bnj1279  29461  bnj1307  29466  bnj1321  29470  bnj1388  29476  bnj1398  29477  bnj1408  29479  bnj1417  29484  bnj1444  29486  bnj1445  29487  bnj1446  29488  bnj1449  29491  bnj1467  29497  bnj1489  29499  bnj1312  29501  bnj1497  29503  bnj1518  29507  bnj1525  29512  bnj1529  29513  spimvNEW7  29595  ax16iNEW7  29625  exsbNEW7  29673  exsbOLDNEW7  29674  equsb3lemNEW7  29675  equsb3NEW7  29676  elsb3NEW7  29677  elsb4NEW7  29678  sbhbwAUX7  29681  sbnf2NEW7  29682  sbid2vNEW7  29686  spimevNEW7  29698  sbiedvNEW7  29706  ax7w15lemxAUX7  29740  ax7w15lemAUX7  29741  ax7w14lemAUX7  29743  ax7w12AUX7  29745  ax7w17lem1AUX7  29749  pm11.53OLD7  29774  19.12vvOLD7  29775  eeanvOLD7  29777  cbvalvOLD7  29802  cbvexvOLD7  29803  cbval2OLD7  29804  cbvex2OLD7  29805  cbval2vOLD7  29806  cbvex2vOLD7  29807  cbvaldvaOLD7  29810  cbvexdvaOLD7  29811  dvelimnfOLD7  29814  ax16ALT2OLD7  29817  sbhbOLD7  29834  dfsb7OLD7  29837  glbconxN  30249  pmapglbx  30640  pmapglb2xN  30643  cdleme26ee  31231  cdleme31sn  31251  cdleme31sn1  31252  cdlemefr29exN  31273  cdlemefs32sn1aw  31285  cdleme43fsv1snlem  31291  cdleme41sn3a  31304  cdleme32fva  31308  cdleme32d  31315  cdleme32f  31317  cdleme40m  31338  cdleme40n  31339  cdleme42b  31349  cdlemk36  31784  cdlemk38  31786  cdlemkid  31807  cdlemk19x  31814  cdlemk11t  31817  dihvalcqpre  32107  mapdheq  32600  hdmap1eq  32674  hdmapval2lem  32706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-17 1627
This theorem depends on definitions:  df-bi 179  df-nf 1555
  Copyright terms: Public domain W3C validator