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

Theorem nfv 1619
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 1616 . 2  |-  ( ph  ->  A. x ph )
21nfi 1551 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1544
This theorem is referenced by:  nfvd  1620  19.21v  1895  19.23v  1896  pm11.53  1898  19.27v  1899  19.28v  1900  19.36v  1901  19.36aiv  1902  19.12vv  1903  19.37v  1904  19.41v  1906  19.42v  1910  eeanv  1918  nexdv  1921  spimv  1995  spimev  2004  cbvalv  2007  cbvexv  2008  cbval2  2009  cbvex2  2010  cbval2v  2011  cbvex2v  2012  cbvaldva  2015  cbvexdva  2016  cleljustALT  2020  dvelimnf  2022  sbiedv  2042  ax16i  2051  ax16ALT2  2053  equsb3lem  2106  equsb3  2107  elsb3  2108  elsb4  2109  sbhb  2112  sbnf2  2113  dfsb7  2124  sbid2v  2128  exsb  2135  exsbOLD  2136  euf  2215  eubidv  2217  nfeud2  2221  sb8eu  2227  mo  2231  euex  2232  euorv  2237  sbmo  2239  mo4f  2241  mo4  2242  mobidv  2244  eu5  2247  moim  2255  morimv  2257  moanim  2265  moanimv  2267  euanv  2270  mopick  2271  moexexv  2279  2mo  2287  2mos  2288  2eu4  2292  2eu6  2294  bm1.1  2343  eqsb3lem  2458  eqsb3  2459  clelsb3  2460  abbi  2468  abbidv  2472  cbvabv  2477  clelab  2478  nfcjust  2482  nfcv  2494  nfeqd  2508  nfeld  2509  nfabd2  2512  dvelimdc  2514  cleqf  2518  sbabel  2520  ralbidva  2635  rexbidva  2636  ralbidv  2639  rexbidv  2640  2ralbida  2658  2ralbidva  2659  ralimdva  2697  ralrimiv  2701  r19.21v  2706  ralrimdv  2708  reximdvai  2729  r19.23v  2735  rexlimiv  2737  rexlimdv  2742  r19.37av  2766  r19.41v  2769  reean  2782  reeanv  2783  reubidva  2799  rmobidva  2804  cbvralf  2834  cbvreu  2838  cbvralv  2840  cbvrexv  2841  cbvreuv  2842  cbvrmov  2843  cbvralsv  2851  cbvrexsv  2852  sbralie  2853  cbvrab  2862  cbvrabv  2863  issetf  2869  ceqsalv  2890  ceqsralv  2891  ceqsexv  2899  ceqsex2  2900  ceqsex2v  2901  vtocld  2912  vtocl  2914  vtoclg  2919  vtocl2g  2923  vtoclga  2925  vtocl2gaf  2926  vtocl2ga  2927  vtocl3gaf  2928  vtocl3ga  2929  spcimdv  2941  spcgv  2944  spcegv  2945  rspct  2953  rspc  2954  rspce  2955  rspcv  2956  rspcev  2960  rspc2v  2966  eqvincf  2972  ceqsexgv  2976  elabgt  2987  elab  2990  elabg  2991  elab3g  2996  elrab  2999  ralab2  3006  rexab2  3008  eqeu  3012  mo2icl  3020  mob2  3021  mob  3023  reu2  3029  reu3  3031  nfcdeq  3064  sbcco  3089  sbcco2  3090  cbvsbcv  3096  sbcieg  3099  sbcie2g  3100  sbcied  3103  elrabsf  3105  sbcbidv  3121  sbcel2gv  3127  sbcg  3132  sbc2iegf  3133  sbc2ie  3134  rmo2  3152  rmo3  3154  csbeq2dv  3182  nfcsb1d  3187  nfcsbd  3190  csbiebt  3193  csbied  3199  csbie2t  3201  sbcnestg  3206  sbnfc2  3217  cbvralcsf  3219  cbvreucsf  3221  cbvrabcsf  3222  cbvralv2  3223  cbvrexv2  3224  dfss2f  3247  uniiunlem  3336  sbss  3639  nfifd  3664  euabsn  3775  nfuni  3912  nfunid  3913  eluniab  3918  nfint  3951  elintab  3952  iineq2dv  4006  disjiun  4092  disjxun  4100  opabbidv  4161  nfopab  4163  cbvopab  4166  cbvopabv  4167  cbvopab1  4168  cbvopab2  4169  cbvopab1s  4170  cbvopab1v  4171  mpteq12f  4175  mpteq2dva  4185  cbvmpt  4189  axrep1  4211  axrep2  4212  axrep3  4213  axrep4  4214  axrep5  4215  zfrepclf  4216  axsep  4219  zfnuleu  4225  eunex  4282  moabex  4311  copsex2t  4332  copsex2g  4333  opelopabaf  4367  nfso  4399  pofun  4409  nffr  4446  reusv2lem2  4615  reusv2lem3  4616  reusv2lem4  4617  reusv2  4619  reusv3  4621  reusv6OLD  4624  alxfr  4626  ralxfrALT  4632  onminex  4677  tfis  4724  tfis2  4726  tfisi  4728  tfinds  4729  tfindes  4732  peano5  4758  findes  4765  opeliunxp  4819  opeliunxp2  4903  ralxpf  4909  dfdmf  4952  dfrnf  4996  elrnmpt1  5007  asymref2  5139  intirr  5140  nfiotad  5301  cbviota  5303  cbviotav  5304  sb8iota  5305  iota2d  5323  iota2  5324  dffun3  5345  dffun6f  5348  fun11  5394  imadif  5406  funimaexg  5408  isarep1  5410  isarep2  5411  fun11iun  5573  fv3  5621  tz6.12f  5626  tz6.12c  5627  funfv2f  5668  fvmptdf  5691  fvmptdv  5692  fvmptt  5695  eqfnfv2f  5706  ralrnmpt  5749  f1ompt  5762  ffnfv  5765  ffnfvf  5766  fmptco  5771  elabrex  5848  abrexex2g  5851  opabex3d  5852  opabex3  5853  abrexex2  5864  dff13f  5868  fliftfun  5895  nfoprab  5984  oprabbidv  5986  mpt2eq123  5991  cbvoprab1  6002  cbvoprab2  6003  cbvoprab12  6004  cbvoprab12v  6005  cbvoprab3  6006  cbvoprab3v  6007  cbvmpt2x  6008  ralrnmpt2  6042  ovmpt2dx  6058  ovmpt2df  6063  ovmpt2dv  6064  ov3  6068  ofrfval2  6180  dfoprab4f  6262  fmpt2x  6274  ovmptss  6284  tposoprab  6354  fvopab5  6373  opabiotafun  6375  cbvriota  6399  cbvriotav  6400  riota2  6411  riota5f  6413  riotasv2d  6433  riotasv2dOLD  6434  riotasv2s  6435  riotasv3d  6437  nfrecs  6474  tfrlem1  6475  tfr3  6499  nfrdg  6511  tz7.48-1  6539  tz7.49  6541  eqerlem  6776  erovlem  6839  mptelixpg  6938  boxcutc  6944  dom2lem  6986  xpf1o  7108  mapxpen  7112  nneneq  7129  isinf  7161  pssnn  7166  findcard2  7185  ac6sfi  7188  fiint  7220  indexfi  7250  wdom2d  7381  ixpiunwdom  7392  sucprcreg  7400  r1val1  7545  rankuni2b  7612  scottexs  7644  scott0s  7645  dfac8clem  7746  acni2  7760  aceq1  7831  dfac5lem5  7841  kmlem14  7876  kmlem15  7877  infpssrlem4  8019  fin23lem27  8041  hsmexlem2  8140  hsmexlem4  8142  axcc3  8151  domtriomlem  8155  axdc3lem2  8164  axdc3lem4  8166  axdc4lem  8168  ac6num  8193  ac6c4  8195  zorn2lem4  8213  zorn2lem5  8214  iunfo  8248  iundom2g  8249  uniimadomf  8254  konigthlem  8277  axrepndlem2  8302  axunnd  8305  axpowndlem2  8307  axpowndlem4  8309  axregndlem2  8312  axacndlem5  8320  zfcndrep  8323  zfcndpow  8325  zfcndinf  8327  zfcndac  8328  pwfseqlem4a  8370  pwfseqlem4  8371  tskuni  8492  gruiin  8519  grothprim  8543  reclem2pr  8759  fimaxre3  9790  uzindOLD  10195  nn0ind-raph  10201  zindd  10202  uzind4s  10367  nnwof  10374  lbzbi  10395  fzrevral  10955  seqof2  11193  rlim2  12060  ello1mpt  12085  climeu  12119  o1compt  12151  cbvsum  12259  summolem2a  12279  zsum  12282  fsum  12284  sumss  12288  sumss2  12290  fsumcvg2  12291  fsum2dlem  12324  fsum00  12347  o1fsum  12362  prmind2  12860  iserodd  12979  pcmpt  13031  pcmptdvds  13033  mreexexd  13643  catpropd  13705  invfuc  13941  natpropd  13943  fucpropd  13944  acsmapd  14374  gsum2d2lem  15317  gsumcom2  15319  dprdwd  15339  dprd2d2  15372  fiuncmp  17231  iunconlem  17253  iuncon  17254  2ndcdisj  17282  elptr2  17369  ptbasfi  17376  ptcld  17407  ptcldmpt  17408  ptclsg  17409  ptcnplem  17415  ptcnp  17416  cnmpt11  17457  cnmpt21  17465  cnmptcom  17472  xkocnv  17605  elmptrab  17618  isfildlem  17648  alexsubALTlem3  17839  ovoliunlem3  18961  ovoliun  18962  ovoliun2  18963  ovoliunnul  18964  finiunmbl  18999  volfiniun  19002  iundisj  19003  iunmbl  19008  voliun  19009  iunmbl2  19012  vitalilem3  19063  mbfeqalem  19095  mbfsup  19117  mbfinf  19118  mbflim  19121  itg2splitlem  19201  itg2split  19202  isibl2  19219  cbvitg  19228  itgeqa  19266  itgss3  19267  itgfsum  19279  itgabs  19287  itggt0  19294  itgcn  19295  limcmpt  19331  limciun  19342  dvmptfsum  19420  dvlipcn  19439  dvfsumlem2  19472  dvfsumlem4  19474  dvfsumrlim  19476  dvfsum2  19479  itgsubst  19494  coeeq2  19722  dgrle  19723  ulmss  19874  leibpi  20343  rlimcnp  20365  rlimcnp2  20366  o1cxp  20374  fsumdvdscom  20531  lgseisenlem2  20695  dchrisumlema  20743  dchrisumlem2  20745  dchrisumlem3  20746  ex-natded9.26  20912  isch3  21929  atom1d  23041  chirred  23083  19.9d2r  23153  r19.29af  23155  r19.29a  23156  clelsb3f  23160  mo5f  23161  rmo4fOLD  23172  rmo4f  23173  elabreximd  23181  elabreximdv  23182  rabss3d  23187  iuninc  23207  cbvdisjf  23211  disjabrex  23220  iundisjf  23224  dfrel4  23239  dfimafnf  23244  suppss2f  23250  ofrn2  23254  cbvmptf  23268  fmptdF  23269  fmpt3d  23270  feqmptdf  23276  fmptcof2  23277  funcnvmptOLD  23282  funcnvmpt  23283  funcnv5mpt  23284  funcnv4mpt  23285  isoun  23290  xrofsup  23324  iundisjfi  23353  ishashinf  23363  neiptoptop  23444  neiptopnei  23445  neiptopreu  23446  lmdvg  23494  cnextfvval  23502  cnextf  23503  ustuqtop  23550  utopsnneiplem  23551  cfilucfil  23603  blval2  23608  restmetu  23615  qqhval2  23639  esumeq12dva  23695  esumeq2dv  23701  esumc  23712  esumadd  23714  gsumesum  23717  esumlub  23718  esumcst  23721  esumpr  23723  esumfzf  23725  esumfsup  23726  esumpfinval  23731  esumpcvgval  23734  esumpmono  23735  esumcocn  23736  hasheuni  23741  esumcvg  23742  sigaclcuni  23767  sigaclfu2  23770  measvunilem  23830  measvunilem0  23831  measvuni  23832  measiuns  23835  measiun  23836  measinblem  23838  voliune  23849  volfiniune  23850  volmeas  23851  dstrvprob  23978  ballotlemelo  23994  ballotleme  24003  ballotlemodife  24004  ballotlemic  24013  ballotlem1c  24014  ballotlemsima  24022  lgamgulmlem2  24063  lgamgulmlem6  24067  lgamcvglem  24073  cvmcov  24198  cvmliftphtlem  24252  untsucf  24460  dedekind  24488  dedekindle  24489  nfcprod1  24537  nfcprod  24538  prodmolem2a  24561  zprod  24564  fprod  24568  fprodntriv  24569  prodss  24574  fprodn0  24604  mpteq12d  24686  setinds2  24694  dfon2lem1  24697  dfon2lem3  24699  wfisg  24767  wfis2g  24771  trpredmintr  24792  frinsg  24803  frins2g  24807  frins2  24808  wfr3g  24813  frr3g  24838  mptelee  25082  quantriv  25398  itgaddnclem2  25499  itgabsnc  25509  itggt0cn  25512  finminlem  25555  upixp  25727  indexa  25736  indexdom  25737  filbcmb  25756  sdclem2  25776  sdclem1  25777  fdc1  25780  totbndbnd  25836  prtlem5  26045  mzpexpmpt  26146  eq0rabdioph  26179  rexrabdioph  26198  rexfrabdioph  26199  elnn0rabdioph  26207  dvdsrabdioph  26214  fphpd  26222  monotuz  26349  monotoddzz  26351  oddcomabszz  26352  setindtr  26440  dford4  26445  wdom2d2  26451  aomclem6  26479  aomclem8  26482  flcidc  26702  pm10.12  26876  19.31vv  26905  aaanv  26910  pm11.57  26911  pm11.58  26912  pm11.59  26913  pm11.71  26919  ax10ext  26929  pm13.192  26933  pm14.12  26944  evth2f  27009  elunif  27010  fvelrnbf  27012  fsumcnf  27015  evthf  27021  fnchoice  27023  sumpair  27029  rfcnnnub  27030  refsum2cn  27032  fmul01  27033  fmuldfeqlem1  27035  fmuldfeq  27036  fmul01lt1lem1  27037  fmul01lt1lem2  27038  fmul01lt1  27039  infrglb  27045  clim1fr1  27050  climexp  27054  climinf  27055  climsuse  27057  climrecf  27058  climinff  27060  stoweidlem3  27075  stoweidlem4  27076  stoweidlem7  27079  stoweidlem14  27086  stoweidlem15  27087  stoweidlem16  27088  stoweidlem17  27089  stoweidlem19  27091  stoweidlem20  27092  stoweidlem26  27098  stoweidlem27  27099  stoweidlem28  27100  stoweidlem29  27101  stoweidlem30  27102  stoweidlem31  27103  stoweidlem34  27106  stoweidlem35  27107  stoweidlem36  27108  stoweidlem39  27111  stoweidlem42  27114  stoweidlem43  27115  stoweidlem44  27116  stoweidlem46  27118  stoweidlem48  27120  stoweidlem49  27121  stoweidlem50  27122  stoweidlem51  27123  stoweidlem52  27124  stoweidlem53  27125  stoweidlem54  27126  stoweidlem56  27128  stoweidlem57  27129  stoweidlem59  27131  stoweidlem60  27132  stoweidlem61  27133  stoweidlem62  27134  stoweid  27135  wallispilem3  27139  wallispi  27142  stirlinglem13  27158  stirlinglem14  27159  stirling  27161  rexsb  27269  rmoanim  27280  2reu4a  27290  ffnafv  27359  ssralv2  28022  tratrb  28027  bnj919  28542  bnj1146  28568  bnj1379  28608  bnj1385  28610  bnj1400  28613  bnj1476  28624  bnj1534  28630  bnj1542  28634  bnj110  28635  bnj121  28647  bnj124  28648  bnj130  28651  bnj207  28658  bnj571  28683  bnj605  28684  bnj580  28690  bnj607  28693  bnj611  28695  bnj873  28701  bnj849  28702  bnj900  28706  bnj916  28710  bnj1000  28718  bnj964  28720  bnj981  28727  bnj985  28730  bnj1014  28737  bnj1123  28761  bnj1128  28765  bnj1228  28786  bnj1204  28787  bnj1279  28793  bnj1307  28798  bnj1321  28802  bnj1388  28808  bnj1398  28809  bnj1408  28811  bnj1417  28816  bnj1444  28818  bnj1445  28819  bnj1446  28820  bnj1449  28823  bnj1467  28829  bnj1489  28831  bnj1312  28833  bnj1497  28835  bnj1518  28839  bnj1525  28844  bnj1529  28845  spimvNEW7  28925  ax16iNEW7  28955  exsbNEW7  29000  exsbOLDNEW7  29001  equsb3lemNEW7  29002  equsb3NEW7  29003  elsb3NEW7  29004  elsb4NEW7  29005  sbhbwAUX7  29008  sbnf2NEW7  29009  sbid2vNEW7  29013  spimevNEW7  29025  cleljustALTNEW7  29029  sbiedvNEW7  29033  pm11.53OLD7  29084  19.12vvOLD7  29085  eeanvOLD7  29087  cbvalvOLD7  29112  cbvexvOLD7  29113  cbval2OLD7  29114  cbvex2OLD7  29115  cbval2vOLD7  29116  cbvex2vOLD7  29117  cbvaldvaOLD7  29120  cbvexdvaOLD7  29121  dvelimnfOLD7  29124  ax16ALT2OLD7  29127  sbhbOLD7  29144  dfsb7OLD7  29149  glbconxN  29619  pmapglbx  30010  pmapglb2xN  30013  cdleme26ee  30601  cdleme31sn  30621  cdleme31sn1  30622  cdlemefr29exN  30643  cdlemefs32sn1aw  30655  cdleme43fsv1snlem  30661  cdleme41sn3a  30674  cdleme32fva  30678  cdleme32d  30685  cdleme32f  30687  cdleme40m  30708  cdleme40n  30709  cdleme42b  30719  cdlemk36  31154  cdlemk38  31156  cdlemkid  31177  cdlemk19x  31184  cdlemk11t  31187  dihvalcqpre  31477  mapdheq  31970  hdmap1eq  32044  hdmapval2lem  32076
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-nf 1545
  Copyright terms: Public domain W3C validator