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  2105  sbiedv  2154  ax16ALT2  2156  equsb3lem  2178  equsb3  2179  elsb3  2180  elsb4  2181  sbhb  2184  sbnf2  2185  pm11.07  2192  dfsb7  2199  sbid2v  2201  exsb  2208  exsbOLD  2209  euf  2288  eubidv  2290  nfeud2  2294  sb8eu  2300  mo  2304  euex  2305  euorv  2310  sbmo  2312  mo4f  2314  mo4  2315  mobidv  2317  eu5  2320  moim  2328  morimv  2330  moanim  2338  moanimv  2340  euanv  2343  mopick  2344  moexexv  2352  2mo  2360  2mos  2361  2eu4  2365  2eu6  2367  bm1.1  2422  eqsb3lem  2537  eqsb3  2538  clelsb3  2539  abbi  2547  abbidv  2551  cbvabv  2556  clelab  2557  nfcjust  2561  nfcv  2573  nfeqd  2587  nfeld  2588  nfabd2  2591  dvelimdc  2593  cleqf  2597  sbabel  2599  ralbidva  2722  rexbidva  2723  ralbidv  2726  rexbidv  2727  2ralbida  2745  2ralbidva  2746  ralimdva  2785  ralrimiv  2789  r19.21v  2794  ralrimdv  2796  reximdvai  2817  r19.23v  2823  rexlimiv  2825  rexlimdv  2830  r19.29af  2850  r19.29a  2851  r19.37av  2859  r19.41v  2862  reean  2875  reeanv  2876  reubidva  2892  rmobidva  2897  cbvralf  2927  cbvreu  2931  cbvralv  2933  cbvrexv  2934  cbvreuv  2935  cbvrmov  2936  cbvralsv  2944  cbvrexsv  2945  sbralie  2946  cbvrab  2955  cbvrabv  2956  issetf  2962  ceqsalv  2983  ceqsralv  2984  ceqsexv  2992  ceqsex2  2993  ceqsex2v  2994  vtocld  3005  vtocl  3007  vtoclg  3012  vtocl2g  3016  vtoclga  3018  vtocl2gaf  3019  vtocl2ga  3020  vtocl3gaf  3021  vtocl3ga  3022  spcimdv  3034  spcgv  3037  spcegv  3038  rspct  3046  rspc  3047  rspce  3048  rspcv  3049  rspcev  3053  rspc2v  3059  eqvincf  3065  ceqsexgv  3069  elabgt  3080  elab  3083  elabg  3084  elab3g  3089  elrab  3093  ralab2  3100  rexab2  3102  eqeu  3106  mo2icl  3114  mob2  3115  mob  3117  reu2  3123  reu3  3125  nfcdeq  3159  sbcco  3184  sbcco2  3185  cbvsbcv  3191  sbcieg  3194  sbcie2g  3195  sbcied  3198  elrabsf  3200  sbcbidv  3216  sbcg  3227  sbc2iegf  3228  sbc2ie  3229  rmo2  3247  rmo3  3249  csbeq2dv  3277  nfcsb1d  3282  nfcsbd  3285  csbiebt  3288  csbied  3294  csbie2t  3296  sbcnestg  3301  sbnfc2  3310  cbvralcsf  3312  cbvreucsf  3314  cbvrabcsf  3315  cbvralv2  3316  cbvrexv2  3317  dfss2f  3340  uniiunlem  3432  sbss  3738  nfifd  3763  euabsn  3877  nfuni  4022  nfunid  4023  eluniab  4028  nfint  4061  elintab  4062  iineq2dv  4116  disjiun  4203  disjxun  4211  opabbidv  4272  nfopab  4274  cbvopab  4277  cbvopabv  4278  cbvopab1  4279  cbvopab2  4280  cbvopab1s  4281  cbvopab1v  4282  mpteq12f  4286  mpteq2dva  4296  cbvmpt  4300  axrep1  4322  axrep2  4323  axrep3  4324  axrep4  4325  axrep5  4326  zfrepclf  4327  axsep  4330  zfnuleu  4336  eunex  4393  moabex  4423  copsex2t  4444  copsex2g  4445  opelopabaf  4479  nfso  4510  pofun  4520  nffr  4557  reusv2lem2  4726  reusv2lem3  4727  reusv2lem4  4728  reusv2  4730  reusv3  4732  reusv6OLD  4735  alxfr  4737  ralxfrALT  4743  onminex  4788  tfis  4835  tfis2  4837  tfisi  4839  tfinds  4840  tfindes  4843  peano5  4869  findes  4876  opeliunxp  4930  opeliunxp2  5014  ralxpf  5020  dfdmf  5065  dfrnf  5109  elrnmpt1  5120  asymref2  5252  intirr  5253  nfiotad  5422  cbviota  5424  cbviotav  5425  sb8iota  5426  iota2d  5444  iota2  5445  dffun3  5466  dffun6f  5469  fun11  5517  imadif  5529  funimaexg  5531  isarep1  5533  isarep2  5534  fun11iun  5696  fv3  5745  tz6.12f  5750  tz6.12c  5751  funfv2f  5793  fvmptdf  5817  fvmptdv  5818  fvmptt  5821  eqfnfv2f  5832  ralrnmpt  5879  f1ompt  5892  ffnfv  5895  ffnfvf  5896  fmptco  5902  elabrex  5986  abrexex2g  5989  opabex3d  5990  opabex3  5991  abrexex2  6002  dff13f  6007  fliftfun  6035  nfoprab  6127  oprabbidv  6129  mpt2eq123  6134  cbvoprab1  6145  cbvoprab2  6146  cbvoprab12  6147  cbvoprab12v  6148  cbvoprab3  6149  cbvoprab3v  6150  cbvmpt2x  6151  ralrnmpt2  6185  ovmpt2dx  6201  ovmpt2df  6206  ovmpt2dv  6207  ov3  6211  ofrfval2  6324  dfoprab4f  6406  fmpt2x  6418  ovmptss  6429  tposoprab  6516  fvopab5  6535  opabiotafun  6537  cbvriota  6561  cbvriotav  6562  riota2  6573  riota5f  6575  riotasv2d  6595  riotasv2dOLD  6596  riotasv2s  6597  riotasv3d  6599  nfrecs  6636  tfrlem1  6637  tfr3  6661  nfrdg  6673  tz7.48-1  6701  tz7.49  6703  eqerlem  6938  erovlem  7001  mptelixpg  7100  boxcutc  7106  dom2lem  7148  xpf1o  7270  mapxpen  7274  nneneq  7291  pssnn  7328  findcard2  7349  ac6sfi  7352  fiint  7384  indexfi  7415  wdom2d  7549  ixpiunwdom  7560  sucprcreg  7568  r1val1  7713  rankuni2b  7780  scottexs  7812  scott0s  7813  dfac8clem  7914  acni2  7928  aceq1  7999  dfac5lem5  8009  kmlem15  8045  infpssrlem4  8187  fin23lem27  8209  hsmexlem2  8308  hsmexlem4  8310  axcc3  8319  domtriomlem  8323  axdc3lem2  8332  axdc3lem4  8334  axdc4lem  8336  ac6num  8360  ac6c4  8362  zorn2lem4  8380  zorn2lem5  8381  iunfo  8415  iundom2g  8416  uniimadomf  8421  konigthlem  8444  axrepndlem2  8469  axunnd  8472  axpowndlem2  8474  axpowndlem4  8476  axregndlem2  8479  axacndlem5  8487  zfcndrep  8490  zfcndpow  8492  zfcndinf  8494  zfcndac  8495  pwfseqlem4a  8537  pwfseqlem4  8538  tskuni  8659  gruiin  8686  grothprim  8710  reclem2pr  8926  fimaxre3  9958  uzindOLD  10365  nn0ind-raph  10371  uzind4s  10537  nnwof  10544  lbzbi  10565  fzrevral  11132  seqof2  11382  rlim2  12291  ello1mpt  12316  climeu  12350  o1compt  12382  summolem2a  12510  zsum  12513  fsum  12515  sumss  12519  sumss2  12521  fsumcvg2  12522  fsum2dlem  12555  fsum00  12578  o1fsum  12593  prmind2  13091  iserodd  13210  pcmpt  13262  pcmptdvds  13264  mreexexd  13874  catpropd  13936  invfuc  14172  natpropd  14174  fucpropd  14175  acsmapd  14605  gsum2d2lem  15548  gsumcom2  15550  dprdwd  15570  dprd2d2  15603  neiptopnei  17197  neiptopreu  17198  neitr  17245  fiuncmp  17468  bwth  17474  iunconlem  17491  iuncon  17492  2ndcdisj  17520  elptr2  17607  ptbasfi  17614  ptcld  17646  ptcldmpt  17647  ptclsg  17648  ptcnplem  17654  ptcnp  17655  cnmpt11  17696  cnmpt21  17704  cnmptcom  17711  imasnopn  17723  imasncld  17724  imasncls  17725  xkocnv  17847  elmptrab  17860  isfildlem  17890  alexsubALTlem3  18081  cnextfvval  18097  utopsnneiplem  18278  isucn2  18310  cfilucfilOLD  18600  cfilucfil  18601  blval2  18606  restmetu  18618  ovoliunlem3  19401  ovoliun  19402  ovoliun2  19403  ovoliunnul  19404  finiunmbl  19439  volfiniun  19442  iundisj  19443  iunmbl  19448  voliun  19449  iunmbl2  19452  mbfeqalem  19535  mbfsup  19557  mbfinf  19558  mbflim  19561  itg2splitlem  19641  itg2split  19642  isibl2  19659  cbvitg  19668  itgeqa  19706  itgss3  19707  itgfsum  19719  itgabs  19727  itggt0  19734  itgcn  19735  limcmpt  19771  limciun  19782  dvmptfsum  19860  dvlipcn  19879  dvfsumlem2  19912  dvfsumlem4  19914  dvfsumrlim  19916  dvfsum2  19919  itgsubst  19934  coeeq2  20162  dgrle  20163  ulmss  20314  leibpi  20783  rlimcnp  20805  rlimcnp2  20806  o1cxp  20814  fsumdvdscom  20971  lgseisenlem2  21135  dchrisumlema  21183  dchrisumlem2  21185  dchrisumlem3  21186  ex-natded9.26  21728  isch3  22745  atom1d  23857  chirred  23899  19.9d2r  23970  clelsb3f  23972  mo5f  23973  rmo4fOLD  23984  rmo4f  23985  elabreximdv  23993  rabss3d  23996  iuninc  24012  cbvdisjf  24016  disjorf  24022  disjabrex  24025  iundisjf  24030  dfrel4  24035  dfimafnf  24044  suppss2f  24050  cbvmptf  24069  feqmptdf  24076  fmptcof2  24077  ofpreima  24082  funcnvmptOLD  24083  funcnv5mpt  24085  funcnv4mpt  24086  xrofsup  24127  iundisjfi  24153  qqhval2  24367  esumeq12dva  24430  esumeq2dv  24436  esumc  24447  esumadd  24449  gsumesum  24452  esumlub  24453  esumpr  24458  esumfzf  24460  esumfsup  24461  esumpcvgval  24469  esumpmono  24470  esumcocn  24471  hasheuni  24476  esumcvg  24477  measvunilem  24567  measvunilem0  24568  measvuni  24569  measiuns  24572  measiun  24573  measinblem  24575  voliune  24586  volfiniune  24587  volmeas  24588  dstrvprob  24730  ballotlemodife  24756  lgamgulmlem2  24815  lgamgulmlem6  24819  cvmcov  24951  untsucf  25160  dedekind  25188  dedekindle  25189  nfcprod1  25237  nfcprod  25238  prodmolem2a  25261  zprod  25264  fprod  25268  fprodntriv  25269  prodss  25274  fprodn0  25304  fprod2dlem  25305  mpteq12d  25397  setinds2  25408  dfon2lem1  25411  dfon2lem3  25413  wfisg  25485  wfis2g  25489  trpredmintr  25510  frinsg  25521  frins2g  25525  frins2  25526  nfwrecs  25534  wfr3g  25538  frr3g  25582  mptelee  25835  itgabsnc  26275  itggt0cn  26278  ftc1anclem5  26285  finminlem  26322  upixp  26432  indexa  26436  indexdom  26437  filbcmb  26443  sdclem2  26447  sdclem1  26448  fdc1  26451  totbndbnd  26499  prtlem5  26706  mzpexpmpt  26803  eq0rabdioph  26836  rexrabdioph  26855  rexfrabdioph  26856  elnn0rabdioph  26864  dvdsrabdioph  26871  fphpd  26878  monotuz  27005  monotoddzz  27007  oddcomabszz  27008  setindtr  27096  dford4  27101  wdom2d2  27107  aomclem6  27135  aomclem8  27137  flcidc  27357  pm10.12  27531  19.31vv  27560  aaanv  27565  pm11.57  27566  pm11.58  27567  pm11.59  27568  pm11.71  27574  ax10ext  27584  pm13.192  27588  pm14.12  27599  evth2f  27663  elunif  27664  fvelrnbf  27666  evthf  27675  fnchoice  27677  sumpair  27683  rfcnnnub  27684  refsum2cn  27686  fmul01  27687  fmuldfeqlem1  27689  fmuldfeq  27690  fmul01lt1lem1  27691  fmul01lt1lem2  27692  fmul01lt1  27693  infrglb  27699  climexp  27708  climsuse  27711  climrecf  27712  climinff  27714  stoweidlem3  27729  stoweidlem14  27740  stoweidlem17  27743  stoweidlem19  27745  stoweidlem20  27746  stoweidlem26  27752  stoweidlem27  27753  stoweidlem28  27754  stoweidlem29  27755  stoweidlem31  27757  stoweidlem34  27760  stoweidlem35  27761  stoweidlem36  27762  stoweidlem39  27765  stoweidlem42  27768  stoweidlem43  27769  stoweidlem44  27770  stoweidlem46  27772  stoweidlem48  27774  stoweidlem49  27775  stoweidlem50  27776  stoweidlem51  27777  stoweidlem52  27778  stoweidlem53  27779  stoweidlem54  27780  stoweidlem56  27782  stoweidlem57  27783  stoweidlem59  27785  stoweidlem60  27786  stoweidlem61  27787  stoweidlem62  27788  stoweid  27789  wallispilem3  27793  stirlinglem13  27812  stirling  27815  rexsb  27923  rmoanim  27934  2reu4a  27944  ffnafv  28012  oprabv  28086  ssralv2  28616  tratrb  28621  iunconlem2  29048  bnj919  29137  bnj1146  29163  bnj1379  29203  bnj1385  29205  bnj1400  29208  bnj1476  29219  bnj1534  29225  bnj1542  29229  bnj110  29230  bnj121  29242  bnj124  29243  bnj130  29246  bnj207  29253  bnj571  29278  bnj605  29279  bnj580  29285  bnj607  29288  bnj611  29290  bnj873  29296  bnj849  29297  bnj900  29301  bnj916  29305  bnj1000  29313  bnj964  29315  bnj981  29322  bnj985  29325  bnj1014  29332  bnj1123  29356  bnj1128  29360  bnj1228  29381  bnj1204  29382  bnj1279  29388  bnj1307  29393  bnj1321  29397  bnj1388  29403  bnj1398  29404  bnj1408  29406  bnj1417  29411  bnj1444  29413  bnj1445  29414  bnj1446  29415  bnj1449  29418  bnj1467  29424  bnj1489  29426  bnj1312  29428  bnj1497  29430  bnj1518  29434  bnj1525  29439  bnj1529  29440  spimvNEW7  29522  ax16iNEW7  29552  exsbNEW7  29600  exsbOLDNEW7  29601  equsb3lemNEW7  29602  equsb3NEW7  29603  elsb3NEW7  29604  elsb4NEW7  29605  sbhbwAUX7  29608  sbnf2NEW7  29609  sbid2vNEW7  29613  spimevNEW7  29625  sbiedvNEW7  29633  ax7w15lemxAUX7  29667  ax7w15lemAUX7  29668  ax7w14lemAUX7  29670  ax7w12AUX7  29672  ax7w17lem1AUX7  29676  pm11.53OLD7  29701  19.12vvOLD7  29702  eeanvOLD7  29704  cbvalvOLD7  29729  cbvexvOLD7  29730  cbval2OLD7  29731  cbvex2OLD7  29732  cbval2vOLD7  29733  cbvex2vOLD7  29734  cbvaldvaOLD7  29737  cbvexdvaOLD7  29738  dvelimnfOLD7  29741  ax16ALT2OLD7  29744  sbhbOLD7  29761  dfsb7OLD7  29764  glbconxN  30176  pmapglbx  30567  pmapglb2xN  30570  cdleme26ee  31158  cdleme31sn  31178  cdleme31sn1  31179  cdlemefr29exN  31200  cdlemefs32sn1aw  31212  cdleme43fsv1snlem  31218  cdleme41sn3a  31231  cdleme32fva  31235  cdleme32d  31242  cdleme32f  31244  cdleme40m  31265  cdleme40n  31266  cdleme42b  31276  cdlemk36  31711  cdlemk38  31713  cdlemkid  31734  cdlemk19x  31741  cdlemk11t  31744  dihvalcqpre  32034  mapdheq  32527  hdmap1eq  32601  hdmapval2lem  32633
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-17 1627
This theorem depends on definitions:  df-bi 179  df-nf 1555
  Copyright terms: Public domain W3C validator