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

Theorem nfv 1606
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 1604 . 2  |-  ( ph  ->  A. x ph )
21nfi 1539 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1532
This theorem is referenced by:  nfvd  1607  19.21v  1833  19.23v  1834  pm11.53  1836  19.27v  1837  19.28v  1838  19.36v  1839  19.36aiv  1840  19.12vv  1841  19.37v  1842  19.41v  1844  19.42v  1848  eeanv  1856  nexdv  1859  spimv  1933  ax16i  1943  spimev  1945  cbvalv  1948  cbvexv  1949  cbval2  1950  cbvex2  1951  cbval2v  1952  cbvex2v  1953  cbvaldva  1956  cbvexdva  1957  cleljustALT  1961  dvelimnf  1963  sbiedv  1983  ax16  1991  equsb3lem  2041  equsb3  2042  elsb3  2043  elsb4  2044  sbhb  2047  sbnf2  2048  dfsb7  2062  sbid2v  2066  exsb  2073  exsbOLD  2074  euf  2151  eubidv  2153  nfeud2  2157  sb8eu  2163  mo  2167  euex  2168  euorv  2173  sbmo  2175  mo4f  2177  mo4  2178  mobidv  2180  eu5  2183  moim  2191  morimv  2193  moanim  2201  moanimv  2203  euanv  2206  mopick  2207  moexexv  2215  2mo  2223  2mos  2224  2eu4  2228  2eu6  2230  bm1.1  2270  eqsb3lem  2385  eqsb3  2386  clelsb3  2387  abbi  2395  abbidv  2399  cbvabv  2404  clelab  2405  nfcjust  2409  nfcv  2421  nfeqd  2435  nfeld  2436  nfabd2  2439  dvelimdc  2441  cleqf  2445  sbabel  2447  ralbidva  2561  rexbidva  2562  ralbidv  2565  rexbidv  2566  2ralbida  2584  2ralbidva  2585  ralimdva  2623  ralrimiv  2627  r19.21v  2632  ralrimdv  2634  reximdvai  2655  r19.23v  2661  rexlimiv  2663  rexlimdv  2668  r19.37av  2692  r19.41v  2695  reean  2708  reeanv  2709  reubidva  2725  rmobidva  2730  cbvralf  2760  cbvreu  2764  cbvralv  2766  cbvrexv  2767  cbvreuv  2768  cbvrmov  2769  cbvralsv  2777  cbvrexsv  2778  sbralie  2779  cbvrab  2788  cbvrabv  2789  issetf  2795  ceqsalv  2816  ceqsralv  2817  ceqsexv  2825  ceqsex2  2826  ceqsex2v  2827  vtocld  2838  vtocl  2840  vtoclg  2845  vtocl2g  2849  vtoclga  2851  vtocl2gaf  2852  vtocl2ga  2853  vtocl3gaf  2854  vtocl3ga  2855  spcimdv  2867  spcgv  2870  spcegv  2871  rspct  2879  rspc  2880  rspce  2881  rspcv  2882  rspcev  2886  rspc2v  2892  eqvincf  2898  ceqsexgv  2902  elabgt  2913  elab  2916  elabg  2917  elab3g  2922  elrab  2925  ralab2  2932  rexab2  2934  eqeu  2938  mo2icl  2946  mob2  2947  mob  2949  reu2  2955  reu3  2957  nfcdeq  2990  sbcco  3015  sbcco2  3016  cbvsbcv  3022  sbcieg  3025  sbcie2g  3026  sbcied  3029  elrabsf  3031  sbcbidv  3047  sbcel2gv  3053  sbcg  3058  sbc2iegf  3059  sbc2ie  3060  rmo2  3078  rmo3  3080  csbeq2dv  3108  nfcsb1d  3113  nfcsbd  3116  csbiebt  3119  csbied  3125  csbie2t  3127  sbcnestg  3132  sbnfc2  3143  cbvralcsf  3145  cbvreucsf  3147  cbvrabcsf  3148  cbvralv2  3149  cbvrexv2  3150  dfss2f  3173  uniiunlem  3262  sbss  3565  nfifd  3590  euabsn  3701  nfuni  3835  nfunid  3836  eluniab  3841  nfint  3874  elintab  3875  iineq2dv  3929  disjiun  4015  disjxun  4023  opabbidv  4084  nfopab  4086  cbvopab  4089  cbvopabv  4090  cbvopab1  4091  cbvopab2  4092  cbvopab1s  4093  cbvopab1v  4094  mpteq12f  4098  mpteq2dva  4108  cbvmpt  4112  axrep1  4134  axrep2  4135  axrep3  4136  axrep4  4137  axrep5  4138  zfrepclf  4139  axsep  4142  zfnuleu  4148  eunex  4203  moabex  4232  copsex2t  4253  copsex2g  4254  opelopabaf  4288  nfso  4320  pofun  4330  nffr  4367  reusv2lem2  4536  reusv2lem3  4537  reusv2lem4  4538  reusv2  4540  reusv3  4542  reusv6OLD  4545  alxfr  4547  ralxfrALT  4553  onminex  4598  tfis  4645  tfis2  4647  tfisi  4649  tfinds  4650  tfindes  4653  peano5  4679  findes  4686  opeliunxp  4740  opeliunxp2  4824  ralxpf  4830  dfdmf  4873  dfrnf  4917  elrnmpt1  4928  asymref2  5060  intirr  5061  dffun3  5233  dffun6f  5236  fun11  5281  imadif  5293  funimaexg  5295  isarep1  5297  isarep2  5298  fun11iun  5459  fv3  5502  tz6.12f  5507  tz6.12c  5509  funfv2f  5550  fvmptdf  5573  fvmptdv  5574  fvmptt  5577  eqfnfv2f  5588  ralrnmpt  5631  f1ompt  5644  ffnfv  5647  ffnfvf  5648  fmptco  5653  elabrex  5727  abrexex2g  5730  opabex3  5731  abrexex2  5742  dff13f  5746  fliftfun  5773  nfoprab  5862  oprabbidv  5864  mpt2eq123  5869  cbvoprab1  5880  cbvoprab2  5881  cbvoprab12  5882  cbvoprab12v  5883  cbvoprab3  5884  cbvoprab3v  5885  cbvmpt2x  5886  ralrnmpt2  5920  ovmpt2dx  5936  ovmpt2df  5941  ovmpt2dv  5942  ov3  5946  ofrfval2  6058  dfoprab4f  6140  fmpt2x  6152  ovmptss  6162  tposoprab  6232  nfiotad  6256  cbviota  6258  cbviotav  6259  sb8iota  6260  iota2d  6278  iota2  6279  fvopab5  6283  opabiotafun  6285  cbvriota  6311  cbvriotav  6312  riota2  6323  riota5f  6325  riotasv2d  6345  riotasv2dOLD  6346  riotasv2s  6347  riotasv3d  6349  nfrecs  6386  tfrlem1  6387  tfr3  6411  nfrdg  6423  tz7.48-1  6451  tz7.49  6453  eqerlem  6688  erovlem  6750  mptelixpg  6849  boxcutc  6855  dom2lem  6897  xpf1o  7019  mapxpen  7023  nneneq  7040  isinf  7072  pssnn  7077  findcard2  7094  ac6sfi  7097  fiint  7129  indexfi  7159  wdom2d  7290  ixpiunwdom  7301  sucprcreg  7309  r1val1  7454  rankuni2b  7521  scottexs  7553  scott0s  7554  dfac8clem  7655  acni2  7669  aceq1  7740  dfac5lem5  7750  kmlem14  7785  kmlem15  7786  infpssrlem4  7928  fin23lem27  7950  hsmexlem2  8049  hsmexlem4  8051  axcc3  8060  domtriomlem  8064  axdc3lem2  8073  axdc3lem4  8075  axdc4lem  8077  ac6num  8102  ac6c4  8104  zorn2lem4  8122  zorn2lem5  8123  iunfo  8157  iundom2g  8158  uniimadomf  8163  konigthlem  8186  axrepndlem2  8211  axunnd  8214  axpowndlem2  8216  axpowndlem4  8218  axregndlem2  8221  axacndlem5  8229  zfcndrep  8232  zfcndpow  8234  zfcndinf  8236  zfcndac  8237  pwfseqlem4a  8279  pwfseqlem4  8280  tskuni  8401  gruiin  8428  grothprim  8452  reclem2pr  8668  fimaxre3  9699  uzindOLD  10102  nn0ind-raph  10108  zindd  10109  uzind4s  10274  nnwof  10281  lbzbi  10302  fzrevral  10861  rlim2  11965  ello1mpt  11990  climeu  12024  o1compt  12056  cbvsum  12163  summolem2a  12183  zsum  12186  fsum  12188  sumss  12192  sumss2  12194  fsumcvg2  12195  fsum2dlem  12228  fsum00  12251  o1fsum  12266  prmind2  12764  iserodd  12883  pcmpt  12935  pcmptdvds  12937  mreexexd  13545  catpropd  13607  invfuc  13843  natpropd  13845  fucpropd  13846  acsmapd  14276  gsum2d2lem  15219  gsumcom2  15221  dprdwd  15241  dprd2d2  15274  fiuncmp  17126  iunconlem  17148  iuncon  17149  2ndcdisj  17177  elptr2  17264  ptbasfi  17271  ptcld  17302  ptcldmpt  17303  ptclsg  17304  ptcnplem  17310  ptcnp  17311  cnmpt11  17352  cnmpt21  17360  cnmptcom  17367  xkocnv  17500  elmptrab  17517  isfildlem  17547  alexsubALTlem3  17738  ovoliunlem3  18858  ovoliun  18859  ovoliun2  18860  ovoliunnul  18861  finiunmbl  18896  volfiniun  18899  iundisj  18900  iunmbl  18905  voliun  18906  iunmbl2  18909  vitalilem3  18960  mbfeqalem  18992  mbfsup  19014  mbfinf  19015  mbflim  19018  itg2splitlem  19098  itg2split  19099  isibl2  19116  cbvitg  19125  itgeqa  19163  itgss3  19164  itgfsum  19176  itgabs  19184  itggt0  19191  itgcn  19192  limcmpt  19228  limciun  19239  dvmptfsum  19317  dvlipcn  19336  dvfsumlem2  19369  dvfsumlem4  19371  dvfsumrlim  19373  dvfsum2  19376  itgsubst  19391  coeeq2  19619  dgrle  19620  ulmss  19769  leibpi  20233  rlimcnp  20255  rlimcnp2  20256  o1cxp  20264  fsumdvdscom  20420  lgseisenlem2  20584  dchrisumlema  20632  dchrisumlem2  20634  dchrisumlem3  20635  ex-natded9.26  20827  isch3  21814  atom1d  22926  chirred  22968  elabreximd  23033  dfimafnf  23035  ballotlemelo  23040  ballotleme  23049  ballotlemodife  23050  ballotlemic  23059  ballotlem1c  23060  ballotlemsima  23068  cvmcov  23199  cvmliftphtlem  23253  untsucf  23461  dedekind  23486  dedekindle  23487  mpteq12d  23530  setinds2  23538  dfon2lem1  23541  dfon2lem3  23543  wfisg  23611  wfis2g  23615  trpredmintr  23636  frinsg  23647  frins2g  23651  frins2  23652  wfr3g  23657  frr3g  23682  mptelee  23931  quantriv  24247  imgfldref2  24463  nfprod1  24710  qusp  24942  bwt2  24992  imonclem  25213  ismonc  25214  cmpmon  25215  iepiclem  25223  isepic  25224  isconcl5a  25501  isconcl5ab  25502  finminlem  25631  upixp  25803  indexa  25812  indexdom  25813  filbcmb  25832  sdclem2  25852  sdclem1  25853  fdc1  25856  totbndbnd  25913  prtlem5  26122  mzpexpmpt  26223  eq0rabdioph  26256  rexrabdioph  26275  rexfrabdioph  26276  elnn0rabdioph  26284  dvdsrabdioph  26291  fphpd  26299  monotuz  26426  monotoddzz  26428  oddcomabszz  26429  setindtr  26517  dford4  26522  wdom2d2  26528  aomclem6  26556  aomclem8  26559  flcidc  26779  pm10.12  26953  19.31vv  26982  aaanv  26987  pm11.57  26988  pm11.58  26989  pm11.59  26990  pm11.71  26996  ax10ext  27006  pm13.192  27010  pm14.12  27021  evth2f  27086  elunif  27087  fvelrnbf  27089  fsumcnf  27092  evthf  27098  fnchoice  27100  sumpair  27106  rfcnnnub  27107  refsum2cn  27109  fmul01  27110  fmuldfeqlem1  27112  fmuldfeq  27113  fmul01lt1lem1  27114  fmul01lt1lem2  27115  fmul01lt1  27116  infrglb  27122  clim1fr1  27127  climexp  27131  climinf  27132  climsuse  27134  climrecf  27135  climinff  27137  stoweidlem3  27152  stoweidlem4  27153  stoweidlem7  27156  stoweidlem14  27163  stoweidlem15  27164  stoweidlem16  27165  stoweidlem17  27166  stoweidlem19  27168  stoweidlem20  27169  stoweidlem26  27175  stoweidlem27  27176  stoweidlem28  27177  stoweidlem29  27178  stoweidlem30  27179  stoweidlem31  27180  stoweidlem34  27183  stoweidlem35  27184  stoweidlem36  27185  stoweidlem39  27188  stoweidlem42  27191  stoweidlem43  27192  stoweidlem44  27193  stoweidlem46  27195  stoweidlem48  27197  stoweidlem49  27198  stoweidlem50  27199  stoweidlem51  27200  stoweidlem52  27201  stoweidlem53  27202  stoweidlem54  27203  stoweidlem56  27205  stoweidlem57  27206  stoweidlem59  27208  stoweidlem60  27209  stoweidlem61  27210  stoweidlem62  27211  stoweid  27212  wallispilem3  27216  wallispi  27219  stirlinglem13  27235  stirlinglem14  27236  stirling  27238  rexsb  27326  rmoanim  27337  2reu4a  27347  ffnafv  27413  ssralv2  27566  tratrb  27571  bnj919  28065  bnj1146  28091  bnj1379  28131  bnj1385  28133  bnj1400  28136  bnj1476  28147  bnj1534  28153  bnj1542  28157  bnj110  28158  bnj121  28170  bnj124  28171  bnj130  28174  bnj207  28181  bnj571  28206  bnj605  28207  bnj580  28213  bnj607  28216  bnj611  28218  bnj873  28224  bnj849  28225  bnj900  28229  bnj916  28233  bnj1000  28241  bnj964  28243  bnj981  28250  bnj985  28253  bnj1014  28260  bnj1123  28284  bnj1128  28288  bnj1228  28309  bnj1204  28310  bnj1279  28316  bnj1307  28321  bnj1321  28325  bnj1388  28331  bnj1398  28332  bnj1408  28334  bnj1417  28339  bnj1444  28341  bnj1445  28342  bnj1446  28343  bnj1449  28346  bnj1467  28352  bnj1489  28354  bnj1312  28356  bnj1497  28358  bnj1518  28362  bnj1525  28367  bnj1529  28368  glbconxN  28835  pmapglbx  29226  pmapglb2xN  29229  cdleme26ee  29817  cdleme31sn  29837  cdleme31sn1  29838  cdlemefr29exN  29859  cdlemefs32sn1aw  29871  cdleme43fsv1snlem  29877  cdleme41sn3a  29890  cdleme32fva  29894  cdleme32d  29901  cdleme32f  29903  cdleme40m  29924  cdleme40n  29925  cdleme42b  29935  cdlemk36  30370  cdlemk38  30372  cdlemkid  30393  cdlemk19x  30400  cdlemk11t  30403  dihvalcqpre  30693  mapdheq  31186  hdmap1eq  31260  hdmapval2lem  31292
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-17 1604
This theorem depends on definitions:  df-bi 179  df-nf 1533
  Copyright terms: Public domain W3C validator