Theorem nfv 1551

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

Step	Hyp	Ref	Expression
1		ax-17 1549	. 2 |- ( ph -> A. x ph )
2	1	nfi 1485	1 |- F/ x ph

Syntax hints:   F/wnf 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1472  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484

This theorem is referenced by:  nfvd  1552  alexim  1668  19.37aiv  1698  sbiedv  1812  spimv  1834  spimev  1884  19.36aiv  1925  cbval2  1945  cbvex2  1946  cbval2v  1947  cbvex2v  1948  cbvald  1949  cbvaldva  1952  cbvexdva  1953  eeanv  1960  nfsbv  1975  sbco2h  1992  nfsbt  2004  sbnf2  2009  dfsb7a  2022  sbalyz  2027  sbco4lem  2034  sbco4  2035  dvelimALT  2038  eubidv  2062  sb8eu  2067  nfeudv  2069  nfeud  2070  nfeuv  2072  nfeu  2073  mobidv  2090  mo23  2095  sbmo  2113  mo4  2115  moimv  2120  moanimv  2129  bm1.1  2190  eqsb1lem  2308  eqsb1  2309  clelsb1  2310  clelsb2  2311  abbi  2319  abbidv  2323  cbvabv  2330  clelab  2331  nfcjust  2336  nfcv  2348  clelsb1f  2352  nfeqd  2363  nfeld  2364  nfabdw  2367  nfabd  2368  dvelimdc  2369  cleqf  2373  sbabel  2375  ralbidva  2502  rexbidva  2503  ralbidv  2506  rexbidv  2507  2ralbida  2527  2ralbidva  2528  nfraldya  2541  nfrexdya  2542  rgen2a  2560  ralimdva  2573  ralrimiv  2578  r19.21v  2583  ralrimdv  2585  reximdvai  2606  r19.23v  2615  rexlimiv  2617  rexlimdv  2622  r19.29af  2647  r19.29an  2648  r19.29a  2649  r19.32vr  2654  r19.37av  2659  r19.41v  2662  reean  2675  reeanv  2676  reubidva  2689  rmobidva  2694  cbvralf  2730  cbvrexf  2731  cbvreu  2736  cbvralv  2738  cbvrexv  2739  cbvreuv  2740  cbvrmov  2741  cbvralsv  2754  cbvrexsv  2755  sbralie  2756  cbvrab  2770  cbvrabv  2771  issetf  2779  ceqsalv  2802  ceqsralv  2803  ceqsexv  2811  ceqsex2  2813  ceqsex2v  2814  vtocld  2825  vtocl  2827  vtocl2  2828  vtocl3  2829  vtoclg  2833  vtocl2g  2837  vtoclga  2839  vtocl2gaf  2840  vtocl2ga  2841  vtocl3gaf  2842  vtocl3ga  2843  spcimdv  2857  spcimedv  2859  spcgv  2860  spcegv  2861  rspct  2870  rspc  2871  rspce  2872  rspcv  2873  rspcev  2877  rspc2v  2890  eqvincg  2897  eqvincf  2898  ceqsexgv  2902  elabgt  2914  elab  2917  elabg  2919  elab3g  2924  elrab3t  2928  elrab  2929  ralab2  2937  rexab2  2939  eqeu  2943  mosubt  2950  mo2icl  2952  mob2  2953  mob  2955  reu2  2961  reu3  2963  rmo4f  2971  nfcdeq  2995  sbcco  3020  sbcco2  3021  cbvsbcv  3028  sbcieg  3031  sbcie2g  3032  sbcied  3035  elrabsf  3037  sbcbidv  3057  sbcg  3068  sbc2iegf  3069  sbc2ie  3070  rmo2ilem  3088  rmo3  3090  csbcow  3104  csbeq2dv  3119  nfcsb1d  3124  nfcsbd  3129  csbiebt  3133  csbied  3140  csbie2t  3142  sbcnestg  3147  sbnfc2  3154  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  cbvralv2  3160  cbvrexv2  3161  rspc2vd  3162  dfss2f  3184  uniiunlem  3282  abn0m  3486  rabn0m  3488  rabeq0  3490  abeq0  3491  r19.3rmv  3551  r19.28mv  3553  r19.27mv  3557  raaanv  3567  sbss  3568  nfifd  3598  euabsn  3703  oprcl  3843  nfuni  3856  nfunid  3857  eluniab  3862  nfint  3895  elintab  3896  iineq2dv  3949  disjiun  4040  opabbidv  4111  nfopab  4113  cbvopab  4116  cbvopabv  4117  cbvopab1  4118  cbvopab2  4119  cbvopab1s  4120  cbvopab1v  4121  mpteq12f  4125  mpteq2dva  4135  cbvmptf  4139  cbvmpt  4140  zfrep6  4162  zfnuleu  4169  intexabim  4197  iinexgm  4199  repizf2  4207  bnd  4217  copsex2t  4290  copsex2g  4291  opelopabsb  4307  opelopabaf  4321  pofun  4360  frind  4400  reusv3  4508  alxfr  4509  rexxfrd  4511  ralxfrALT  4515  onintonm  4566  sucprcreg  4598  eunex  4610  tfis  4632  tfis2  4634  tfisi  4636  peano2  4644  findes  4652  omsinds  4671  opeliunxp  4731  opeliunxp2  4819  ralxpf  4825  rexxpf  4826  dfdmf  4872  dfrnf  4920  elrnmpt1  4930  intirr  5070  nfiotadw  5236  cbviota  5238  cbviotav  5239  sb8iota  5240  iota2d  5259  iota2  5262  dffun5r  5284  dffun6f  5285  dffun4f  5288  funco  5312  fun11  5342  imadif  5355  isarep1  5361  isarep2  5362  fun11iun  5545  fv3  5601  tz6.12f  5607  tz6.12c  5608  relelfvdm  5610  nfvres  5612  funimass4  5631  funfvdm2f  5646  fvmptss2  5656  fvmptdf  5669  fvmptdv  5670  fvmptt  5673  eqfnfv2f  5683  ralrnmpt  5724  rexrnmpt  5725  f1ompt  5733  ffnfv  5740  ffnfvf  5741  fmptco  5748  elabrex  5828  elabrexg  5829  dff13f  5841  fliftfun  5867  cbvriota  5912  cbvriotav  5913  riota2  5924  riota5f  5926  acexmid  5945  nfoprab  5999  oprabbidv  6001  mpoeq123  6006  cbvoprab1  6019  cbvoprab2  6020  cbvoprab12  6021  cbvoprab12v  6022  cbvoprab3  6023  cbvoprab3v  6024  cbvmpox  6025  ralrnmpo  6062  ovmpodx  6074  ovmpodf  6079  ovmpodv  6080  ovi3  6085  ofrfval2  6177  abrexex2g  6207  opabex3d  6208  opabex3  6209  abrexex2  6211  uchoice  6225  dfoprab4f  6281  fmpox  6288  spc2ed  6321  cnvoprab  6322  f1od2  6323  opeliunxp2f  6326  tposoprab  6368  nfrecs  6395  tfri3  6455  nffrec  6484  eqerlem  6653  erovlem  6716  mptelixpg  6823  dom2lem  6865  xpf1o  6943  mapxpen  6947  nneneq  6956  findcard2  6988  findcard2s  6989  ac6sfi  6997  fiintim  7030  opabfi  7037  exmidomni  7246  fodjuomnilemdc  7248  ismkvnex  7259  mkvprop  7262  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  cc3  7382  indpi  7457  prarloclem3step  7611  prmuloc2  7682  ltexprlemm  7715  caucvgprprlemaddq  7823  caucvgsrlemgt1  7910  suplocsrlem  7923  axpre-suploclemres  8016  nn0ind-raph  9492  uzind4s  9713  indstr  9716  supinfneg  9718  infsupneg  9719  lbzbi  9739  fzrevral  10229  zsupcllemstep  10374  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  nninfinf  10590  uzsinds  10591  seq3f1olemstep  10661  seq3f1olemp  10662  fimaxre2  11571  climeu  11640  nfsum1  11700  nfsum  11701  sumrbdclem  11721  summodclem2a  11725  zsumdc  11728  fsum3  11731  isumss  11735  isumss2  11737  fsum3cvg2  11738  fsumsplitf  11752  fsum2dlemstep  11778  fsum00  11806  fsumrelem  11815  mertenslem2  11880  nfcprod1  11898  nfcprod  11899  prodeq2  11901  prodrbdclem  11915  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  fprodntrivap  11928  prodssdc  11933  fprodcl2lem  11949  fprod2dlemstep  11966  fprodsplitf  11976  fprodsplit1f  11978  fprodap0f  11980  fprodle  11984  divalglemeunn  12265  divalglemeuneg  12267  bezoutlemnewy  12350  bezoutlemmain  12352  bezoutlemzz  12356  bezout  12365  nnwofdc  12392  prmind2  12475  oddpwdclemdvds  12525  oddpwdclemndvds  12526  pcmpt  12699  pcmptdvds  12701  exmidunben  12830  ctiunctlemfo  12843  ctiunct  12844  ctiunctal  12845  dfgrp3mlem  13463  lss1d  14178  gsumfzfsumlemm  14382  cnmpt11  14788  cnmpt21  14796  cnmptcom  14803  imasnopn  14804  mulcncf  15113  ellimc3apf  15165  limccnp2cntop  15182  dvmptfsum  15230  lgseisenlem2  15581  gropd  15677  grstructd2dom  15678  ch2varv  15741  elab1  15756  elab2a  15757  elabg2  15758  cbvrald  15761  sumdc2  15772  bdsepnft  15860  bdsepnfALT  15862  bj-omssind  15908  bj-bdfindes  15922  bj-nn0suc0  15923  bj-nntrans  15924  bj-nnelirr  15926  bj-omtrans  15929  setindft  15938  bj-inf2vnlem3  15945  bj-inf2vnlem4  15946  bj-nn0sucALT  15951  bj-findis  15952  bj-findes  15954  strcollnft  15957  strcollnfALT  15959  pw1nct  15977  isomninnlem  16006  trilpolemeq1  16016  trirec0  16020  iswomninnlem  16025  ismkvnnlem  16028  nconstwlpolemgt0  16040