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

Theorem nfv 1605
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 1603 . 2  |-  ( ph  ->  A. x ph )
21nfi 1538 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1531
This theorem is referenced by:  nfvd  1606  19.21v  1831  19.23v  1832  pm11.53  1834  19.27v  1835  19.28v  1836  19.36v  1837  19.36aiv  1838  19.12vv  1839  19.37v  1840  19.41v  1842  19.42v  1846  eeanv  1854  nexdv  1857  spimv  1930  spimev  1939  cbvalv  1942  cbvexv  1943  cbval2  1944  cbvex2  1945  cbval2v  1946  cbvex2v  1947  cbvaldva  1950  cbvexdva  1951  cleljustALT  1955  dvelimnf  1957  sbiedv  1977  ax16i  1986  ax16ALT2  1988  equsb3lem  2040  equsb3  2041  elsb3  2042  elsb4  2043  sbhb  2046  sbnf2  2047  dfsb7  2058  sbid2v  2062  exsb  2069  exsbOLD  2070  euf  2149  eubidv  2151  nfeud2  2155  sb8eu  2161  mo  2165  euex  2166  euorv  2171  sbmo  2173  mo4f  2175  mo4  2176  mobidv  2178  eu5  2181  moim  2189  morimv  2191  moanim  2199  moanimv  2201  euanv  2204  mopick  2205  moexexv  2213  2mo  2221  2mos  2222  2eu4  2226  2eu6  2228  bm1.1  2268  eqsb3lem  2383  eqsb3  2384  clelsb3  2385  abbi  2393  abbidv  2397  cbvabv  2402  clelab  2403  nfcjust  2407  nfcv  2419  nfeqd  2433  nfeld  2434  nfabd2  2437  dvelimdc  2439  cleqf  2443  sbabel  2445  ralbidva  2559  rexbidva  2560  ralbidv  2563  rexbidv  2564  2ralbida  2582  2ralbidva  2583  ralimdva  2621  ralrimiv  2625  r19.21v  2630  ralrimdv  2632  reximdvai  2653  r19.23v  2659  rexlimiv  2661  rexlimdv  2666  r19.37av  2690  r19.41v  2693  reean  2706  reeanv  2707  reubidva  2723  rmobidva  2728  cbvralf  2758  cbvreu  2762  cbvralv  2764  cbvrexv  2765  cbvreuv  2766  cbvrmov  2767  cbvralsv  2775  cbvrexsv  2776  sbralie  2777  cbvrab  2786  cbvrabv  2787  issetf  2793  ceqsalv  2814  ceqsralv  2815  ceqsexv  2823  ceqsex2  2824  ceqsex2v  2825  vtocld  2836  vtocl  2838  vtoclg  2843  vtocl2g  2847  vtoclga  2849  vtocl2gaf  2850  vtocl2ga  2851  vtocl3gaf  2852  vtocl3ga  2853  spcimdv  2865  spcgv  2868  spcegv  2869  rspct  2877  rspc  2878  rspce  2879  rspcv  2880  rspcev  2884  rspc2v  2890  eqvincf  2896  ceqsexgv  2900  elabgt  2911  elab  2914  elabg  2915  elab3g  2920  elrab  2923  ralab2  2930  rexab2  2932  eqeu  2936  mo2icl  2944  mob2  2945  mob  2947  reu2  2953  reu3  2955  nfcdeq  2988  sbcco  3013  sbcco2  3014  cbvsbcv  3020  sbcieg  3023  sbcie2g  3024  sbcied  3027  elrabsf  3029  sbcbidv  3045  sbcel2gv  3051  sbcg  3056  sbc2iegf  3057  sbc2ie  3058  rmo2  3076  rmo3  3078  csbeq2dv  3106  nfcsb1d  3111  nfcsbd  3114  csbiebt  3117  csbied  3123  csbie2t  3125  sbcnestg  3130  sbnfc2  3141  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  cbvralv2  3147  cbvrexv2  3148  dfss2f  3171  uniiunlem  3260  sbss  3563  nfifd  3588  euabsn  3699  nfuni  3833  nfunid  3834  eluniab  3839  nfint  3872  elintab  3873  iineq2dv  3927  disjiun  4013  disjxun  4021  opabbidv  4082  nfopab  4084  cbvopab  4087  cbvopabv  4088  cbvopab1  4089  cbvopab2  4090  cbvopab1s  4091  cbvopab1v  4092  mpteq12f  4096  mpteq2dva  4106  cbvmpt  4110  axrep1  4132  axrep2  4133  axrep3  4134  axrep4  4135  axrep5  4136  zfrepclf  4137  axsep  4140  zfnuleu  4146  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  nfiotad  5222  cbviota  5224  cbviotav  5225  sb8iota  5226  iota2d  5244  iota2  5245  dffun3  5266  dffun6f  5269  fun11  5315  imadif  5327  funimaexg  5329  isarep1  5331  isarep2  5332  fun11iun  5493  fv3  5541  tz6.12f  5546  tz6.12c  5547  funfv2f  5588  fvmptdf  5611  fvmptdv  5612  fvmptt  5615  eqfnfv2f  5626  ralrnmpt  5669  f1ompt  5682  ffnfv  5685  ffnfvf  5686  fmptco  5691  elabrex  5765  abrexex2g  5768  opabex3  5769  abrexex2  5780  dff13f  5784  fliftfun  5811  nfoprab  5900  oprabbidv  5902  mpt2eq123  5907  cbvoprab1  5918  cbvoprab2  5919  cbvoprab12  5920  cbvoprab12v  5921  cbvoprab3  5922  cbvoprab3v  5923  cbvmpt2x  5924  ralrnmpt2  5958  ovmpt2dx  5974  ovmpt2df  5979  ovmpt2dv  5980  ov3  5984  ofrfval2  6096  dfoprab4f  6178  fmpt2x  6190  ovmptss  6200  tposoprab  6270  fvopab5  6289  opabiotafun  6291  cbvriota  6315  cbvriotav  6316  riota2  6327  riota5f  6329  riotasv2d  6349  riotasv2dOLD  6350  riotasv2s  6351  riotasv3d  6353  nfrecs  6390  tfrlem1  6391  tfr3  6415  nfrdg  6427  tz7.48-1  6455  tz7.49  6457  eqerlem  6692  erovlem  6754  mptelixpg  6853  boxcutc  6859  dom2lem  6901  xpf1o  7023  mapxpen  7027  nneneq  7044  isinf  7076  pssnn  7081  findcard2  7098  ac6sfi  7101  fiint  7133  indexfi  7163  wdom2d  7294  ixpiunwdom  7305  sucprcreg  7313  r1val1  7458  rankuni2b  7525  scottexs  7557  scott0s  7558  dfac8clem  7659  acni2  7673  aceq1  7744  dfac5lem5  7754  kmlem14  7789  kmlem15  7790  infpssrlem4  7932  fin23lem27  7954  hsmexlem2  8053  hsmexlem4  8055  axcc3  8064  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  ac6num  8106  ac6c4  8108  zorn2lem4  8126  zorn2lem5  8127  iunfo  8161  iundom2g  8162  uniimadomf  8167  konigthlem  8190  axrepndlem2  8215  axunnd  8218  axpowndlem2  8220  axpowndlem4  8222  axregndlem2  8225  axacndlem5  8233  zfcndrep  8236  zfcndpow  8238  zfcndinf  8240  zfcndac  8241  pwfseqlem4a  8283  pwfseqlem4  8284  tskuni  8405  gruiin  8432  grothprim  8456  reclem2pr  8672  fimaxre3  9703  uzindOLD  10106  nn0ind-raph  10112  zindd  10113  uzind4s  10278  nnwof  10285  lbzbi  10306  fzrevral  10866  rlim2  11970  ello1mpt  11995  climeu  12029  o1compt  12061  cbvsum  12168  summolem2a  12188  zsum  12191  fsum  12193  sumss  12197  sumss2  12199  fsumcvg2  12200  fsum2dlem  12233  fsum00  12256  o1fsum  12271  prmind2  12769  iserodd  12888  pcmpt  12940  pcmptdvds  12942  mreexexd  13550  catpropd  13612  invfuc  13848  natpropd  13850  fucpropd  13851  acsmapd  14281  gsum2d2lem  15224  gsumcom2  15226  dprdwd  15246  dprd2d2  15279  fiuncmp  17131  iunconlem  17153  iuncon  17154  2ndcdisj  17182  elptr2  17269  ptbasfi  17276  ptcld  17307  ptcldmpt  17308  ptclsg  17309  ptcnplem  17315  ptcnp  17316  cnmpt11  17357  cnmpt21  17365  cnmptcom  17372  xkocnv  17505  elmptrab  17522  isfildlem  17552  alexsubALTlem3  17743  ovoliunlem3  18863  ovoliun  18864  ovoliun2  18865  ovoliunnul  18866  finiunmbl  18901  volfiniun  18904  iundisj  18905  iunmbl  18910  voliun  18911  iunmbl2  18914  vitalilem3  18965  mbfeqalem  18997  mbfsup  19019  mbfinf  19020  mbflim  19023  itg2splitlem  19103  itg2split  19104  isibl2  19121  cbvitg  19130  itgeqa  19168  itgss3  19169  itgfsum  19181  itgabs  19189  itggt0  19196  itgcn  19197  limcmpt  19233  limciun  19244  dvmptfsum  19322  dvlipcn  19341  dvfsumlem2  19374  dvfsumlem4  19376  dvfsumrlim  19378  dvfsum2  19381  itgsubst  19396  coeeq2  19624  dgrle  19625  ulmss  19774  leibpi  20238  rlimcnp  20260  rlimcnp2  20261  o1cxp  20269  fsumdvdscom  20425  lgseisenlem2  20589  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  ex-natded9.26  20806  isch3  21821  atom1d  22933  chirred  22975  elabreximd  23039  dfimafnf  23041  ballotlemelo  23046  ballotleme  23055  ballotlemodife  23056  ballotlemic  23065  ballotlem1c  23066  ballotlemsima  23074  rabss3d  23136  clelsb3f  23142  mo5f  23143  iuninc  23158  rmo4fOLD  23179  rmo4f  23180  19.9d2r  23183  elabreximdv  23193  suppss2f  23201  dfrel4  23204  ofrn2  23207  cbvmptf  23220  fmptdF  23221  fmpt3d  23222  feqmptdf  23228  fmptcof2  23229  funcnvmptOLD  23234  funcnvmpt  23235  funcnv5mpt  23236  funcnv4mpt  23237  isoun  23242  xrofsup  23255  cbvdisjf  23350  disjabrex  23359  iundisjfi  23363  iundisjf  23365  lmdvg  23376  ishashinf  23389  esumeq12dva  23415  esumeq2dv  23420  esumc  23430  esumadd  23432  esumcst  23436  esumpr  23438  esumpfinval  23443  esumpcvgval  23446  esumpmono  23447  esumcocn  23448  hasheuni  23453  esumcvg  23454  sigaclcuni  23479  sigaclfu2  23482  measvunilem  23540  measvunilem0  23541  measvuni  23542  measiuns  23544  measiun  23545  measinblem  23547  dya2iocseg  23579  dstrvprob  23672  cvmcov  23794  cvmliftphtlem  23848  untsucf  24056  dedekind  24082  dedekindle  24083  mpteq12d  24128  setinds2  24136  dfon2lem1  24139  dfon2lem3  24141  wfisg  24209  wfis2g  24213  trpredmintr  24234  frinsg  24245  frins2g  24249  frins2  24250  wfr3g  24255  frr3g  24280  mptelee  24523  quantriv  24839  imgfldref2  25064  nfprod1  25310  qusp  25542  bwt2  25592  imonclem  25813  ismonc  25814  cmpmon  25815  iepiclem  25823  isepic  25824  isconcl5a  26101  isconcl5ab  26102  finminlem  26231  upixp  26403  indexa  26412  indexdom  26413  filbcmb  26432  sdclem2  26452  sdclem1  26453  fdc1  26456  totbndbnd  26513  prtlem5  26722  mzpexpmpt  26823  eq0rabdioph  26856  rexrabdioph  26875  rexfrabdioph  26876  elnn0rabdioph  26884  dvdsrabdioph  26891  fphpd  26899  monotuz  27026  monotoddzz  27028  oddcomabszz  27029  setindtr  27117  dford4  27122  wdom2d2  27128  aomclem6  27156  aomclem8  27159  flcidc  27379  pm10.12  27553  19.31vv  27582  aaanv  27587  pm11.57  27588  pm11.58  27589  pm11.59  27590  pm11.71  27596  ax10ext  27606  pm13.192  27610  pm14.12  27621  evth2f  27686  elunif  27687  fvelrnbf  27689  fsumcnf  27692  evthf  27698  fnchoice  27700  sumpair  27706  rfcnnnub  27707  refsum2cn  27709  fmul01  27710  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  fmul01lt1  27716  infrglb  27722  clim1fr1  27727  climexp  27731  climinf  27732  climsuse  27734  climrecf  27735  climinff  27737  stoweidlem3  27752  stoweidlem4  27753  stoweidlem7  27756  stoweidlem14  27763  stoweidlem15  27764  stoweidlem16  27765  stoweidlem17  27766  stoweidlem19  27768  stoweidlem20  27769  stoweidlem26  27775  stoweidlem27  27776  stoweidlem28  27777  stoweidlem29  27778  stoweidlem30  27779  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem36  27785  stoweidlem39  27788  stoweidlem42  27791  stoweidlem43  27792  stoweidlem44  27793  stoweidlem46  27795  stoweidlem48  27797  stoweidlem49  27798  stoweidlem50  27799  stoweidlem51  27800  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  stoweidlem56  27805  stoweidlem57  27806  stoweidlem59  27808  stoweidlem60  27809  stoweidlem61  27810  stoweidlem62  27811  stoweid  27812  wallispilem3  27816  wallispi  27819  stirlinglem13  27835  stirlinglem14  27836  stirling  27838  rexsb  27946  rmoanim  27957  2reu4a  27967  ffnafv  28033  ssralv2  28294  tratrb  28299  bnj919  28797  bnj1146  28823  bnj1379  28863  bnj1385  28865  bnj1400  28868  bnj1476  28879  bnj1534  28885  bnj1542  28889  bnj110  28890  bnj121  28902  bnj124  28903  bnj130  28906  bnj207  28913  bnj571  28938  bnj605  28939  bnj580  28945  bnj607  28948  bnj611  28950  bnj873  28956  bnj849  28957  bnj900  28961  bnj916  28965  bnj1000  28973  bnj964  28975  bnj981  28982  bnj985  28985  bnj1014  28992  bnj1123  29016  bnj1128  29020  bnj1228  29041  bnj1204  29042  bnj1279  29048  bnj1307  29053  bnj1321  29057  bnj1388  29063  bnj1398  29064  bnj1408  29066  bnj1417  29071  bnj1444  29073  bnj1445  29074  bnj1446  29075  bnj1449  29078  bnj1467  29084  bnj1489  29086  bnj1312  29088  bnj1497  29090  bnj1518  29094  bnj1525  29099  bnj1529  29100  glbconxN  29567  pmapglbx  29958  pmapglb2xN  29961  cdleme26ee  30549  cdleme31sn  30569  cdleme31sn1  30570  cdlemefr29exN  30591  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdleme41sn3a  30622  cdleme32fva  30626  cdleme32d  30633  cdleme32f  30635  cdleme40m  30656  cdleme40n  30657  cdleme42b  30667  cdlemk36  31102  cdlemk38  31104  cdlemkid  31125  cdlemk19x  31132  cdlemk11t  31135  dihvalcqpre  31425  mapdheq  31918  hdmap1eq  31992  hdmapval2lem  32024
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator