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  19.21v  1902  19.23v  1903  pm11.53  1905  19.27v  1906  19.28v  1907  19.36v  1908  19.36aiv  1909  19.12vv  1910  19.37v  1911  19.41v  1913  19.42v  1917  eeanv  1926  eeeanv  1927  nexdv  1930  spimv  1953  ax12olem4  1963  dvelimv  1975  spimev  2033  cbvalv  2036  cbvexv  2037  cbval2  2038  cbvex2  2039  cbval2v  2040  cbvex2v  2041  cbvaldva  2044  cbvexdva  2045  cleljustALT  2049  dvelimnf  2051  sbiedv  2070  ax16i  2079  ax16ALT2  2081  equsb3lem  2134  equsb3  2135  elsb3  2136  elsb4  2137  sbhb  2140  sbnf2  2141  pm11.07  2148  dfsb7  2155  sbid2v  2157  exsb  2164  exsbOLD  2165  euf  2244  eubidv  2246  nfeud2  2250  sb8eu  2256  mo  2260  euex  2261  euorv  2266  sbmo  2268  mo4f  2270  mo4  2271  mobidv  2273  eu5  2276  moim  2284  morimv  2286  moanim  2294  moanimv  2296  euanv  2299  mopick  2300  moexexv  2308  2mo  2316  2mos  2317  2eu4  2321  2eu6  2323  bm1.1  2372  eqsb3lem  2487  eqsb3  2488  clelsb3  2489  abbi  2497  abbidv  2501  cbvabv  2506  clelab  2507  nfcjust  2511  nfcv  2523  nfeqd  2537  nfeld  2538  nfabd2  2541  dvelimdc  2543  cleqf  2547  sbabel  2549  ralbidva  2665  rexbidva  2666  ralbidv  2669  rexbidv  2670  2ralbida  2688  2ralbidva  2689  ralimdva  2727  ralrimiv  2731  r19.21v  2736  ralrimdv  2738  reximdvai  2759  r19.23v  2765  rexlimiv  2767  rexlimdv  2772  r19.29af  2792  r19.29a  2793  r19.37av  2801  r19.41v  2804  reean  2817  reeanv  2818  reubidva  2834  rmobidva  2839  cbvralf  2869  cbvreu  2873  cbvralv  2875  cbvrexv  2876  cbvreuv  2877  cbvrmov  2878  cbvralsv  2886  cbvrexsv  2887  sbralie  2888  cbvrab  2897  cbvrabv  2898  issetf  2904  ceqsalv  2925  ceqsralv  2926  ceqsexv  2934  ceqsex2  2935  ceqsex2v  2936  vtocld  2947  vtocl  2949  vtoclg  2954  vtocl2g  2958  vtoclga  2960  vtocl2gaf  2961  vtocl2ga  2962  vtocl3gaf  2963  vtocl3ga  2964  spcimdv  2976  spcgv  2979  spcegv  2980  rspct  2988  rspc  2989  rspce  2990  rspcv  2991  rspcev  2995  rspc2v  3001  eqvincf  3007  ceqsexgv  3011  elabgt  3022  elab  3025  elabg  3026  elab3g  3031  elrab  3035  ralab2  3042  rexab2  3044  eqeu  3048  mo2icl  3056  mob2  3057  mob  3059  reu2  3065  reu3  3067  nfcdeq  3101  sbcco  3126  sbcco2  3127  cbvsbcv  3133  sbcieg  3136  sbcie2g  3137  sbcied  3140  elrabsf  3142  sbcbidv  3158  sbcg  3169  sbc2iegf  3170  sbc2ie  3171  rmo2  3189  rmo3  3191  csbeq2dv  3219  nfcsb1d  3224  nfcsbd  3227  csbiebt  3230  csbied  3236  csbie2t  3238  sbcnestg  3243  sbnfc2  3252  cbvralcsf  3254  cbvreucsf  3256  cbvrabcsf  3257  cbvralv2  3258  cbvrexv2  3259  dfss2f  3282  uniiunlem  3374  sbss  3680  nfifd  3705  euabsn  3819  nfuni  3963  nfunid  3964  eluniab  3969  nfint  4002  elintab  4003  iineq2dv  4057  disjiun  4143  disjxun  4151  opabbidv  4212  nfopab  4214  cbvopab  4217  cbvopabv  4218  cbvopab1  4219  cbvopab2  4220  cbvopab1s  4221  cbvopab1v  4222  mpteq12f  4226  mpteq2dva  4236  cbvmpt  4240  axrep1  4262  axrep2  4263  axrep3  4264  axrep4  4265  axrep5  4266  zfrepclf  4267  axsep  4270  zfnuleu  4276  eunex  4333  moabex  4363  copsex2t  4384  copsex2g  4385  opelopabaf  4419  nfso  4450  pofun  4460  nffr  4497  reusv2lem2  4665  reusv2lem3  4666  reusv2lem4  4667  reusv2  4669  reusv3  4671  reusv6OLD  4674  alxfr  4676  ralxfrALT  4682  onminex  4727  tfis  4774  tfis2  4776  tfisi  4778  tfinds  4779  tfindes  4782  peano5  4808  findes  4815  opeliunxp  4869  opeliunxp2  4953  ralxpf  4959  dfdmf  5004  dfrnf  5048  elrnmpt1  5059  asymref2  5191  intirr  5192  nfiotad  5361  cbviota  5363  cbviotav  5364  sb8iota  5365  iota2d  5383  iota2  5384  dffun3  5405  dffun6f  5408  fun11  5456  imadif  5468  funimaexg  5470  isarep1  5472  isarep2  5473  fun11iun  5635  fv3  5684  tz6.12f  5689  tz6.12c  5690  funfv2f  5731  fvmptdf  5755  fvmptdv  5756  fvmptt  5759  eqfnfv2f  5770  ralrnmpt  5817  f1ompt  5830  ffnfv  5833  ffnfvf  5834  fmptco  5840  elabrex  5924  abrexex2g  5927  opabex3d  5928  opabex3  5929  abrexex2  5940  dff13f  5945  fliftfun  5973  nfoprab  6065  oprabbidv  6067  mpt2eq123  6072  cbvoprab1  6083  cbvoprab2  6084  cbvoprab12  6085  cbvoprab12v  6086  cbvoprab3  6087  cbvoprab3v  6088  cbvmpt2x  6089  ralrnmpt2  6123  ovmpt2dx  6139  ovmpt2df  6144  ovmpt2dv  6145  ov3  6149  ofrfval2  6262  dfoprab4f  6344  fmpt2x  6356  ovmptss  6367  tposoprab  6451  fvopab5  6470  opabiotafun  6472  cbvriota  6496  cbvriotav  6497  riota2  6508  riota5f  6510  riotasv2d  6530  riotasv2dOLD  6531  riotasv2s  6532  riotasv3d  6534  nfrecs  6571  tfrlem1  6572  tfr3  6596  nfrdg  6608  tz7.48-1  6636  tz7.49  6638  eqerlem  6873  erovlem  6936  mptelixpg  7035  boxcutc  7041  dom2lem  7083  xpf1o  7205  mapxpen  7209  nneneq  7226  pssnn  7263  findcard2  7284  ac6sfi  7287  fiint  7319  indexfi  7349  wdom2d  7481  ixpiunwdom  7492  sucprcreg  7500  r1val1  7645  rankuni2b  7712  scottexs  7744  scott0s  7745  dfac8clem  7846  acni2  7860  aceq1  7931  dfac5lem5  7941  kmlem15  7977  infpssrlem4  8119  fin23lem27  8141  hsmexlem2  8240  hsmexlem4  8242  axcc3  8251  domtriomlem  8255  axdc3lem2  8264  axdc3lem4  8266  axdc4lem  8268  ac6num  8292  ac6c4  8294  zorn2lem4  8312  zorn2lem5  8313  iunfo  8347  iundom2g  8348  uniimadomf  8353  konigthlem  8376  axrepndlem2  8401  axunnd  8404  axpowndlem2  8406  axpowndlem4  8408  axregndlem2  8411  axacndlem5  8419  zfcndrep  8422  zfcndpow  8424  zfcndinf  8426  zfcndac  8427  pwfseqlem4a  8469  pwfseqlem4  8470  tskuni  8591  gruiin  8618  grothprim  8642  reclem2pr  8858  fimaxre3  9889  uzindOLD  10296  nn0ind-raph  10302  uzind4s  10468  nnwof  10475  lbzbi  10496  fzrevral  11061  seqof2  11308  rlim2  12217  ello1mpt  12242  climeu  12276  o1compt  12308  summolem2a  12436  zsum  12439  fsum  12441  sumss  12445  sumss2  12447  fsumcvg2  12448  fsum2dlem  12481  fsum00  12504  o1fsum  12519  prmind2  13017  iserodd  13136  pcmpt  13188  pcmptdvds  13190  mreexexd  13800  catpropd  13862  invfuc  14098  natpropd  14100  fucpropd  14101  acsmapd  14531  gsum2d2lem  15474  gsumcom2  15476  dprdwd  15496  dprd2d2  15529  neiptopnei  17119  neiptopreu  17120  neitr  17166  fiuncmp  17389  iunconlem  17411  iuncon  17412  2ndcdisj  17440  elptr2  17527  ptbasfi  17534  ptcld  17566  ptcldmpt  17567  ptclsg  17568  ptcnplem  17574  ptcnp  17575  cnmpt11  17616  cnmpt21  17624  cnmptcom  17631  imasnopn  17643  imasncld  17644  imasncls  17645  xkocnv  17767  elmptrab  17780  isfildlem  17810  alexsubALTlem3  18001  cnextfvval  18017  utopsnneiplem  18198  isucn2  18230  cfilucfil  18479  blval2  18482  restmetu  18489  ovoliunlem3  19267  ovoliun  19268  ovoliun2  19269  ovoliunnul  19270  finiunmbl  19305  volfiniun  19308  iundisj  19309  iunmbl  19314  voliun  19315  iunmbl2  19318  mbfeqalem  19401  mbfsup  19423  mbfinf  19424  mbflim  19427  itg2splitlem  19507  itg2split  19508  isibl2  19525  cbvitg  19534  itgeqa  19572  itgss3  19573  itgfsum  19585  itgabs  19593  itggt0  19600  itgcn  19601  limcmpt  19637  limciun  19648  dvmptfsum  19726  dvlipcn  19745  dvfsumlem2  19778  dvfsumlem4  19780  dvfsumrlim  19782  dvfsum2  19785  itgsubst  19800  coeeq2  20028  dgrle  20029  ulmss  20180  leibpi  20649  rlimcnp  20671  rlimcnp2  20672  o1cxp  20680  fsumdvdscom  20837  lgseisenlem2  21001  dchrisumlema  21049  dchrisumlem2  21051  dchrisumlem3  21052  ex-natded9.26  21575  isch3  22592  atom1d  23704  chirred  23746  19.9d2r  23813  clelsb3f  23815  mo5f  23816  rmo4fOLD  23827  rmo4f  23828  elabreximdv  23836  rabss3d  23839  iuninc  23855  cbvdisjf  23859  disjorf  23865  disjabrex  23868  iundisjf  23872  dfrel4  23877  dfimafnf  23886  suppss2f  23892  cbvmptf  23910  feqmptdf  23917  fmptcof2  23918  funcnvmptOLD  23923  funcnv5mpt  23925  funcnv4mpt  23926  xrofsup  23962  iundisjfi  23990  qqhval2  24165  esumeq12dva  24225  esumeq2dv  24231  esumc  24242  esumadd  24244  gsumesum  24247  esumlub  24248  esumpr  24253  esumfzf  24255  esumfsup  24256  esumpcvgval  24264  esumpmono  24265  esumcocn  24266  hasheuni  24271  esumcvg  24272  measvunilem  24360  measvunilem0  24361  measvuni  24362  measiuns  24365  measiun  24366  measinblem  24368  voliune  24379  volfiniune  24380  volmeas  24381  dstrvprob  24508  ballotlemodife  24534  lgamgulmlem2  24593  lgamgulmlem6  24597  cvmcov  24729  untsucf  24938  dedekind  24966  dedekindle  24967  nfcprod1  25015  nfcprod  25016  prodmolem2a  25039  zprod  25042  fprod  25046  fprodntriv  25047  prodss  25052  fprodn0  25082  mpteq12d  25152  setinds2  25160  dfon2lem1  25163  dfon2lem3  25165  wfisg  25233  wfis2g  25237  trpredmintr  25258  frinsg  25269  frins2g  25273  frins2  25274  wfr3g  25279  frr3g  25304  mptelee  25548  itgaddnclem2  25964  itgabsnc  25974  itggt0cn  25977  finminlem  26012  upixp  26122  indexa  26126  indexdom  26127  filbcmb  26133  sdclem2  26137  sdclem1  26138  fdc1  26141  totbndbnd  26189  prtlem5  26396  mzpexpmpt  26493  eq0rabdioph  26526  rexrabdioph  26545  rexfrabdioph  26546  elnn0rabdioph  26554  dvdsrabdioph  26561  fphpd  26568  monotuz  26695  monotoddzz  26697  oddcomabszz  26698  setindtr  26786  dford4  26791  wdom2d2  26797  aomclem6  26825  aomclem8  26828  flcidc  27048  pm10.12  27222  19.31vv  27251  aaanv  27256  pm11.57  27257  pm11.58  27258  pm11.59  27259  pm11.71  27265  ax10ext  27275  pm13.192  27279  pm14.12  27290  evth2f  27354  elunif  27355  fvelrnbf  27357  evthf  27366  fnchoice  27368  sumpair  27374  rfcnnnub  27375  refsum2cn  27377  fmul01  27378  fmuldfeqlem1  27380  fmuldfeq  27381  fmul01lt1lem1  27382  fmul01lt1lem2  27383  fmul01lt1  27384  infrglb  27390  climexp  27399  climsuse  27402  climrecf  27403  climinff  27405  stoweidlem3  27420  stoweidlem14  27431  stoweidlem17  27434  stoweidlem19  27436  stoweidlem20  27437  stoweidlem26  27443  stoweidlem27  27444  stoweidlem28  27445  stoweidlem29  27446  stoweidlem31  27448  stoweidlem34  27451  stoweidlem35  27452  stoweidlem36  27453  stoweidlem39  27456  stoweidlem42  27459  stoweidlem43  27460  stoweidlem44  27461  stoweidlem46  27463  stoweidlem48  27465  stoweidlem49  27466  stoweidlem50  27467  stoweidlem51  27468  stoweidlem52  27469  stoweidlem53  27470  stoweidlem54  27471  stoweidlem56  27473  stoweidlem57  27474  stoweidlem59  27476  stoweidlem60  27477  stoweidlem61  27478  stoweidlem62  27479  stoweid  27480  wallispilem3  27484  stirlinglem13  27503  stirling  27506  rexsb  27614  rmoanim  27625  2reu4a  27635  ffnafv  27704  ssralv2  27958  tratrb  27963  bnj919  28474  bnj1146  28500  bnj1379  28540  bnj1385  28542  bnj1400  28545  bnj1476  28556  bnj1534  28562  bnj1542  28566  bnj110  28567  bnj121  28579  bnj124  28580  bnj130  28583  bnj207  28590  bnj571  28615  bnj605  28616  bnj580  28622  bnj607  28625  bnj611  28627  bnj873  28633  bnj849  28634  bnj900  28638  bnj916  28642  bnj1000  28650  bnj964  28652  bnj981  28659  bnj985  28662  bnj1014  28669  bnj1123  28693  bnj1128  28697  bnj1228  28718  bnj1204  28719  bnj1279  28725  bnj1307  28730  bnj1321  28734  bnj1388  28740  bnj1398  28741  bnj1408  28743  bnj1417  28748  bnj1444  28750  bnj1445  28751  bnj1446  28752  bnj1449  28755  bnj1467  28761  bnj1489  28763  bnj1312  28765  bnj1497  28767  bnj1518  28771  bnj1525  28776  bnj1529  28777  spimvNEW7  28857  ax16iNEW7  28887  exsbNEW7  28932  exsbOLDNEW7  28933  equsb3lemNEW7  28934  equsb3NEW7  28935  elsb3NEW7  28936  elsb4NEW7  28937  sbhbwAUX7  28940  sbnf2NEW7  28941  sbid2vNEW7  28945  spimevNEW7  28957  sbiedvNEW7  28965  pm11.53OLD7  29016  19.12vvOLD7  29017  eeanvOLD7  29019  cbvalvOLD7  29044  cbvexvOLD7  29045  cbval2OLD7  29046  cbvex2OLD7  29047  cbval2vOLD7  29048  cbvex2vOLD7  29049  cbvaldvaOLD7  29052  cbvexdvaOLD7  29053  dvelimnfOLD7  29056  ax16ALT2OLD7  29059  sbhbOLD7  29076  dfsb7OLD7  29080  glbconxN  29492  pmapglbx  29883  pmapglb2xN  29886  cdleme26ee  30474  cdleme31sn  30494  cdleme31sn1  30495  cdlemefr29exN  30516  cdlemefs32sn1aw  30528  cdleme43fsv1snlem  30534  cdleme41sn3a  30547  cdleme32fva  30551  cdleme32d  30558  cdleme32f  30560  cdleme40m  30581  cdleme40n  30582  cdleme42b  30592  cdlemk36  31027  cdlemk38  31029  cdlemkid  31050  cdlemk19x  31057  cdlemk11t  31060  dihvalcqpre  31350  mapdheq  31843  hdmap1eq  31917  hdmapval2lem  31949
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