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

Theorem nfv 1609
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 1606 . 2  |-  ( ph  ->  A. x ph )
21nfi 1541 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1534
This theorem is referenced by:  nfvd  1610  19.21v  1843  19.23v  1844  pm11.53  1846  19.27v  1847  19.28v  1848  19.36v  1849  19.36aiv  1850  19.12vv  1851  19.37v  1852  19.41v  1854  19.42v  1858  eeanv  1866  nexdv  1869  spimv  1943  spimev  1952  cbvalv  1955  cbvexv  1956  cbval2  1957  cbvex2  1958  cbval2v  1959  cbvex2v  1960  cbvaldva  1963  cbvexdva  1964  cleljustALT  1968  dvelimnf  1970  sbiedv  1990  ax16i  1999  ax16ALT2  2001  equsb3lem  2053  equsb3  2054  elsb3  2055  elsb4  2056  sbhb  2059  sbnf2  2060  dfsb7  2071  sbid2v  2075  exsb  2082  exsbOLD  2083  euf  2162  eubidv  2164  nfeud2  2168  sb8eu  2174  mo  2178  euex  2179  euorv  2184  sbmo  2186  mo4f  2188  mo4  2189  mobidv  2191  eu5  2194  moim  2202  morimv  2204  moanim  2212  moanimv  2214  euanv  2217  mopick  2218  moexexv  2226  2mo  2234  2mos  2235  2eu4  2239  2eu6  2241  bm1.1  2281  eqsb3lem  2396  eqsb3  2397  clelsb3  2398  abbi  2406  abbidv  2410  cbvabv  2415  clelab  2416  nfcjust  2420  nfcv  2432  nfeqd  2446  nfeld  2447  nfabd2  2450  dvelimdc  2452  cleqf  2456  sbabel  2458  ralbidva  2572  rexbidva  2573  ralbidv  2576  rexbidv  2577  2ralbida  2595  2ralbidva  2596  ralimdva  2634  ralrimiv  2638  r19.21v  2643  ralrimdv  2645  reximdvai  2666  r19.23v  2672  rexlimiv  2674  rexlimdv  2679  r19.37av  2703  r19.41v  2706  reean  2719  reeanv  2720  reubidva  2736  rmobidva  2741  cbvralf  2771  cbvreu  2775  cbvralv  2777  cbvrexv  2778  cbvreuv  2779  cbvrmov  2780  cbvralsv  2788  cbvrexsv  2789  sbralie  2790  cbvrab  2799  cbvrabv  2800  issetf  2806  ceqsalv  2827  ceqsralv  2828  ceqsexv  2836  ceqsex2  2837  ceqsex2v  2838  vtocld  2849  vtocl  2851  vtoclg  2856  vtocl2g  2860  vtoclga  2862  vtocl2gaf  2863  vtocl2ga  2864  vtocl3gaf  2865  vtocl3ga  2866  spcimdv  2878  spcgv  2881  spcegv  2882  rspct  2890  rspc  2891  rspce  2892  rspcv  2893  rspcev  2897  rspc2v  2903  eqvincf  2909  ceqsexgv  2913  elabgt  2924  elab  2927  elabg  2928  elab3g  2933  elrab  2936  ralab2  2943  rexab2  2945  eqeu  2949  mo2icl  2957  mob2  2958  mob  2960  reu2  2966  reu3  2968  nfcdeq  3001  sbcco  3026  sbcco2  3027  cbvsbcv  3033  sbcieg  3036  sbcie2g  3037  sbcied  3040  elrabsf  3042  sbcbidv  3058  sbcel2gv  3064  sbcg  3069  sbc2iegf  3070  sbc2ie  3071  rmo2  3089  rmo3  3091  csbeq2dv  3119  nfcsb1d  3124  nfcsbd  3127  csbiebt  3130  csbied  3136  csbie2t  3138  sbcnestg  3143  sbnfc2  3154  cbvralcsf  3156  cbvreucsf  3158  cbvrabcsf  3159  cbvralv2  3160  cbvrexv2  3161  dfss2f  3184  uniiunlem  3273  sbss  3576  nfifd  3601  euabsn  3712  nfuni  3849  nfunid  3850  eluniab  3855  nfint  3888  elintab  3889  iineq2dv  3943  disjiun  4029  disjxun  4037  opabbidv  4098  nfopab  4100  cbvopab  4103  cbvopabv  4104  cbvopab1  4105  cbvopab2  4106  cbvopab1s  4107  cbvopab1v  4108  mpteq12f  4112  mpteq2dva  4122  cbvmpt  4126  axrep1  4148  axrep2  4149  axrep3  4150  axrep4  4151  axrep5  4152  zfrepclf  4153  axsep  4156  zfnuleu  4162  eunex  4219  moabex  4248  copsex2t  4269  copsex2g  4270  opelopabaf  4304  nfso  4336  pofun  4346  nffr  4383  reusv2lem2  4552  reusv2lem3  4553  reusv2lem4  4554  reusv2  4556  reusv3  4558  reusv6OLD  4561  alxfr  4563  ralxfrALT  4569  onminex  4614  tfis  4661  tfis2  4663  tfisi  4665  tfinds  4666  tfindes  4669  peano5  4695  findes  4702  opeliunxp  4756  opeliunxp2  4840  ralxpf  4846  dfdmf  4889  dfrnf  4933  elrnmpt1  4944  asymref2  5076  intirr  5077  nfiotad  5238  cbviota  5240  cbviotav  5241  sb8iota  5242  iota2d  5260  iota2  5261  dffun3  5282  dffun6f  5285  fun11  5331  imadif  5343  funimaexg  5345  isarep1  5347  isarep2  5348  fun11iun  5509  fv3  5557  tz6.12f  5562  tz6.12c  5563  funfv2f  5604  fvmptdf  5627  fvmptdv  5628  fvmptt  5631  eqfnfv2f  5642  ralrnmpt  5685  f1ompt  5698  ffnfv  5701  ffnfvf  5702  fmptco  5707  elabrex  5781  abrexex2g  5784  opabex3  5785  abrexex2  5796  dff13f  5800  fliftfun  5827  nfoprab  5916  oprabbidv  5918  mpt2eq123  5923  cbvoprab1  5934  cbvoprab2  5935  cbvoprab12  5936  cbvoprab12v  5937  cbvoprab3  5938  cbvoprab3v  5939  cbvmpt2x  5940  ralrnmpt2  5974  ovmpt2dx  5990  ovmpt2df  5995  ovmpt2dv  5996  ov3  6000  ofrfval2  6112  dfoprab4f  6194  fmpt2x  6206  ovmptss  6216  tposoprab  6286  fvopab5  6305  opabiotafun  6307  cbvriota  6331  cbvriotav  6332  riota2  6343  riota5f  6345  riotasv2d  6365  riotasv2dOLD  6366  riotasv2s  6367  riotasv3d  6369  nfrecs  6406  tfrlem1  6407  tfr3  6431  nfrdg  6443  tz7.48-1  6471  tz7.49  6473  eqerlem  6708  erovlem  6770  mptelixpg  6869  boxcutc  6875  dom2lem  6917  xpf1o  7039  mapxpen  7043  nneneq  7060  isinf  7092  pssnn  7097  findcard2  7114  ac6sfi  7117  fiint  7149  indexfi  7179  wdom2d  7310  ixpiunwdom  7321  sucprcreg  7329  r1val1  7474  rankuni2b  7541  scottexs  7573  scott0s  7574  dfac8clem  7675  acni2  7689  aceq1  7760  dfac5lem5  7770  kmlem14  7805  kmlem15  7806  infpssrlem4  7948  fin23lem27  7970  hsmexlem2  8069  hsmexlem4  8071  axcc3  8080  domtriomlem  8084  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  ac6num  8122  ac6c4  8124  zorn2lem4  8142  zorn2lem5  8143  iunfo  8177  iundom2g  8178  uniimadomf  8183  konigthlem  8206  axrepndlem2  8231  axunnd  8234  axpowndlem2  8236  axpowndlem4  8238  axregndlem2  8241  axacndlem5  8249  zfcndrep  8252  zfcndpow  8254  zfcndinf  8256  zfcndac  8257  pwfseqlem4a  8299  pwfseqlem4  8300  tskuni  8421  gruiin  8448  grothprim  8472  reclem2pr  8688  fimaxre3  9719  uzindOLD  10122  nn0ind-raph  10128  zindd  10129  uzind4s  10294  nnwof  10301  lbzbi  10322  fzrevral  10882  rlim2  11986  ello1mpt  12011  climeu  12045  o1compt  12077  cbvsum  12184  summolem2a  12204  zsum  12207  fsum  12209  sumss  12213  sumss2  12215  fsumcvg2  12216  fsum2dlem  12249  fsum00  12272  o1fsum  12287  prmind2  12785  iserodd  12904  pcmpt  12956  pcmptdvds  12958  mreexexd  13566  catpropd  13628  invfuc  13864  natpropd  13866  fucpropd  13867  acsmapd  14297  gsum2d2lem  15240  gsumcom2  15242  dprdwd  15262  dprd2d2  15295  fiuncmp  17147  iunconlem  17169  iuncon  17170  2ndcdisj  17198  elptr2  17285  ptbasfi  17292  ptcld  17323  ptcldmpt  17324  ptclsg  17325  ptcnplem  17331  ptcnp  17332  cnmpt11  17373  cnmpt21  17381  cnmptcom  17388  xkocnv  17521  elmptrab  17538  isfildlem  17568  alexsubALTlem3  17759  ovoliunlem3  18879  ovoliun  18880  ovoliun2  18881  ovoliunnul  18882  finiunmbl  18917  volfiniun  18920  iundisj  18921  iunmbl  18926  voliun  18927  iunmbl2  18930  vitalilem3  18981  mbfeqalem  19013  mbfsup  19035  mbfinf  19036  mbflim  19039  itg2splitlem  19119  itg2split  19120  isibl2  19137  cbvitg  19146  itgeqa  19184  itgss3  19185  itgfsum  19197  itgabs  19205  itggt0  19212  itgcn  19213  limcmpt  19249  limciun  19260  dvmptfsum  19338  dvlipcn  19357  dvfsumlem2  19390  dvfsumlem4  19392  dvfsumrlim  19394  dvfsum2  19397  itgsubst  19412  coeeq2  19640  dgrle  19641  ulmss  19790  leibpi  20254  rlimcnp  20276  rlimcnp2  20277  o1cxp  20285  fsumdvdscom  20441  lgseisenlem2  20605  dchrisumlema  20653  dchrisumlem2  20655  dchrisumlem3  20656  ex-natded9.26  20822  isch3  21837  atom1d  22949  chirred  22991  elabreximd  23055  dfimafnf  23057  ballotlemelo  23062  ballotleme  23071  ballotlemodife  23072  ballotlemic  23081  ballotlem1c  23082  ballotlemsima  23090  rabss3d  23152  clelsb3f  23158  mo5f  23159  iuninc  23174  rmo4fOLD  23195  rmo4f  23196  19.9d2r  23199  elabreximdv  23208  suppss2f  23216  dfrel4  23219  ofrn2  23222  cbvmptf  23235  fmptdF  23236  fmpt3d  23237  feqmptdf  23243  fmptcof2  23244  funcnvmptOLD  23249  funcnvmpt  23250  funcnv5mpt  23251  funcnv4mpt  23252  isoun  23257  xrofsup  23270  cbvdisjf  23365  disjabrex  23374  iundisjfi  23378  iundisjf  23380  lmdvg  23391  ishashinf  23404  esumeq12dva  23430  esumeq2dv  23435  esumc  23445  esumadd  23447  esumcst  23451  esumpr  23453  esumpfinval  23458  esumpcvgval  23461  esumpmono  23462  esumcocn  23463  hasheuni  23468  esumcvg  23469  sigaclcuni  23494  sigaclfu2  23497  measvunilem  23555  measvunilem0  23556  measvuni  23557  measiuns  23559  measiun  23560  measinblem  23562  dya2iocseg  23594  dstrvprob  23687  cvmcov  23809  cvmliftphtlem  23863  untsucf  24071  dedekind  24097  dedekindle  24098  nfcprod1  24132  nfcprod  24133  prodmolem2a  24157  zprod  24160  fprod  24164  mpteq12d  24198  setinds2  24206  dfon2lem1  24209  dfon2lem3  24211  wfisg  24279  wfis2g  24283  trpredmintr  24304  frinsg  24315  frins2g  24319  frins2  24320  wfr3g  24325  frr3g  24350  mptelee  24594  quantriv  24910  itgaddnclem2  25009  itgabsnc  25019  itggt0cn  25022  imgfldref2  25166  nfprod1  25412  qusp  25644  bwt2  25694  imonclem  25915  ismonc  25916  cmpmon  25917  iepiclem  25925  isepic  25926  isconcl5a  26203  isconcl5ab  26204  finminlem  26333  upixp  26505  indexa  26514  indexdom  26515  filbcmb  26534  sdclem2  26554  sdclem1  26555  fdc1  26558  totbndbnd  26615  prtlem5  26824  mzpexpmpt  26925  eq0rabdioph  26958  rexrabdioph  26977  rexfrabdioph  26978  elnn0rabdioph  26986  dvdsrabdioph  26993  fphpd  27001  monotuz  27128  monotoddzz  27130  oddcomabszz  27131  setindtr  27219  dford4  27224  wdom2d2  27230  aomclem6  27258  aomclem8  27261  flcidc  27481  pm10.12  27655  19.31vv  27684  aaanv  27689  pm11.57  27690  pm11.58  27691  pm11.59  27692  pm11.71  27698  ax10ext  27708  pm13.192  27712  pm14.12  27723  evth2f  27788  elunif  27789  fvelrnbf  27791  fsumcnf  27794  evthf  27800  fnchoice  27802  sumpair  27808  rfcnnnub  27809  refsum2cn  27811  fmul01  27812  fmuldfeqlem1  27814  fmuldfeq  27815  fmul01lt1lem1  27816  fmul01lt1lem2  27817  fmul01lt1  27818  infrglb  27824  clim1fr1  27829  climexp  27833  climinf  27834  climsuse  27836  climrecf  27837  climinff  27839  stoweidlem3  27854  stoweidlem4  27855  stoweidlem7  27858  stoweidlem14  27865  stoweidlem15  27866  stoweidlem16  27867  stoweidlem17  27868  stoweidlem19  27870  stoweidlem20  27871  stoweidlem26  27877  stoweidlem27  27878  stoweidlem28  27879  stoweidlem29  27880  stoweidlem30  27881  stoweidlem31  27882  stoweidlem34  27885  stoweidlem35  27886  stoweidlem36  27887  stoweidlem39  27890  stoweidlem42  27893  stoweidlem43  27894  stoweidlem44  27895  stoweidlem46  27897  stoweidlem48  27899  stoweidlem49  27900  stoweidlem50  27901  stoweidlem51  27902  stoweidlem52  27903  stoweidlem53  27904  stoweidlem54  27905  stoweidlem56  27907  stoweidlem57  27908  stoweidlem59  27910  stoweidlem60  27911  stoweidlem61  27912  stoweidlem62  27913  stoweid  27914  wallispilem3  27918  wallispi  27921  stirlinglem13  27937  stirlinglem14  27938  stirling  27940  rexsb  28048  rmoanim  28059  2reu4a  28069  ffnafv  28138  opabex3d  28189  ssralv2  28592  tratrb  28597  bnj919  29112  bnj1146  29138  bnj1379  29178  bnj1385  29180  bnj1400  29183  bnj1476  29194  bnj1534  29200  bnj1542  29204  bnj110  29205  bnj121  29217  bnj124  29218  bnj130  29221  bnj207  29228  bnj571  29253  bnj605  29254  bnj580  29260  bnj607  29263  bnj611  29265  bnj873  29271  bnj849  29272  bnj900  29276  bnj916  29280  bnj1000  29288  bnj964  29290  bnj981  29297  bnj985  29300  bnj1014  29307  bnj1123  29331  bnj1128  29335  bnj1228  29356  bnj1204  29357  bnj1279  29363  bnj1307  29368  bnj1321  29372  bnj1388  29378  bnj1398  29379  bnj1408  29381  bnj1417  29386  bnj1444  29388  bnj1445  29389  bnj1446  29390  bnj1449  29393  bnj1467  29399  bnj1489  29401  bnj1312  29403  bnj1497  29405  bnj1518  29409  bnj1525  29414  bnj1529  29415  spimvNEW7  29495  ax16iNEW7  29525  exsbNEW7  29570  exsbOLDNEW7  29571  equsb3lemNEW7  29572  equsb3NEW7  29573  elsb3NEW7  29574  elsb4NEW7  29575  sbhbwAUX7  29578  sbnf2NEW7  29579  sbid2vNEW7  29583  spimevNEW7  29595  cleljustALTNEW7  29599  sbiedvNEW7  29603  pm11.53OLD7  29654  19.12vvOLD7  29655  eeanvOLD7  29657  cbvalvOLD7  29682  cbvexvOLD7  29683  cbval2OLD7  29684  cbvex2OLD7  29685  cbval2vOLD7  29686  cbvex2vOLD7  29687  cbvaldvaOLD7  29690  cbvexdvaOLD7  29691  dvelimnfOLD7  29694  ax16ALT2OLD7  29697  sbhbOLD7  29714  dfsb7OLD7  29719  glbconxN  30189  pmapglbx  30580  pmapglb2xN  30583  cdleme26ee  31171  cdleme31sn  31191  cdleme31sn1  31192  cdlemefr29exN  31213  cdlemefs32sn1aw  31225  cdleme43fsv1snlem  31231  cdleme41sn3a  31244  cdleme32fva  31248  cdleme32d  31255  cdleme32f  31257  cdleme40m  31278  cdleme40n  31279  cdleme42b  31289  cdlemk36  31724  cdlemk38  31726  cdlemkid  31747  cdlemk19x  31754  cdlemk11t  31757  dihvalcqpre  32047  mapdheq  32540  hdmap1eq  32614  hdmapval2lem  32646
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-17 1606
This theorem depends on definitions:  df-bi 177  df-nf 1535
  Copyright terms: Public domain W3C validator