Theorem nfv 1509

Description: If 𝑥 is not present in 𝜑, then 𝑥 is not free in 𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfv	⊢ Ⅎ𝑥𝜑

Distinct variable group:   𝜑,𝑥

Proof of Theorem nfv

Step	Hyp	Ref	Expression
1		ax-17 1507	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2	1	nfi 1439	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:  Ⅎwnf 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1426  ax-17 1507

This theorem depends on definitions:  df-bi 116  df-nf 1438

This theorem is referenced by:  nfvd  1510  alexim  1625  19.37aiv  1654  sbiedv  1763  spimv  1784  spimev  1834  19.36aiv  1874  cbval2  1894  cbvex2  1895  cbval2v  1896  cbvex2v  1897  cbvald  1898  cbvaldva  1901  cbvexdva  1902  eeanv  1905  sbco2h  1938  nfsbt  1950  sbnf2  1957  dfsb7a  1970  sbalyz  1975  sbco4lem  1982  sbco4  1983  dvelimALT  1986  eubidv  2008  sb8eu  2013  nfeudv  2015  nfeud  2016  nfeuv  2018  nfeu  2019  mobidv  2036  mo23  2041  sbmo  2059  mo4  2061  moimv  2066  moanimv  2075  bm1.1  2125  eqsb3lem  2243  eqsb3  2244  clelsb3  2245  clelsb4  2246  abbi  2254  abbidv  2258  cbvabv  2265  clelab  2266  nfcjust  2270  nfcv  2282  clelsb3f  2286  nfeqd  2297  nfeld  2298  nfabd  2301  dvelimdc  2302  cleqf  2306  sbabel  2308  ralbidva  2434  rexbidva  2435  ralbidv  2438  rexbidv  2439  2ralbida  2459  2ralbidva  2460  nfraldya  2472  nfrexdya  2473  rgen2a  2489  ralimdva  2502  ralrimiv  2507  r19.21v  2512  ralrimdv  2514  reximdvai  2535  r19.23v  2544  rexlimiv  2546  rexlimdv  2551  r19.29af  2576  r19.29an  2577  r19.29a  2578  r19.32vr  2582  r19.37av  2587  r19.41v  2590  reean  2602  reeanv  2603  reubidva  2616  rmobidva  2621  cbvralf  2651  cbvrexf  2652  cbvreu  2655  cbvralv  2657  cbvrexv  2658  cbvreuv  2659  cbvrmov  2660  cbvralsv  2671  cbvrexsv  2672  sbralie  2673  cbvrab  2687  cbvrabv  2688  issetf  2696  ceqsalv  2719  ceqsralv  2720  ceqsexv  2728  ceqsex2  2729  ceqsex2v  2730  vtocld  2741  vtocl  2743  vtocl2  2744  vtocl3  2745  vtoclg  2749  vtocl2g  2753  vtoclga  2755  vtocl2gaf  2756  vtocl2ga  2757  vtocl3gaf  2758  vtocl3ga  2759  spcimdv  2773  spcimedv  2775  spcgv  2776  spcegv  2777  rspct  2786  rspc  2787  rspce  2788  rspcv  2789  rspcev  2793  rspc2v  2806  eqvincg  2813  eqvincf  2814  ceqsexgv  2818  elabgt  2829  elab  2832  elabg  2834  elab3g  2839  elrab3t  2843  elrab  2844  ralab2  2852  rexab2  2854  eqeu  2858  mosubt  2865  mo2icl  2867  mob2  2868  mob  2870  reu2  2876  reu3  2878  rmo4f  2886  nfcdeq  2910  sbcco  2934  sbcco2  2935  cbvsbcv  2942  sbcieg  2945  sbcie2g  2946  sbcied  2949  elrabsf  2951  sbcbidv  2971  sbcg  2982  sbc2iegf  2983  sbc2ie  2984  rmo2ilem  3002  rmo3  3004  csbeq2dv  3033  nfcsb1d  3038  nfcsbd  3041  csbiebt  3044  csbied  3051  csbie2t  3053  sbcnestg  3058  sbnfc2  3065  cbvralcsf  3067  cbvrexcsf  3068  cbvreucsf  3069  cbvrabcsf  3070  cbvralv2  3071  cbvrexv2  3072  dfss2f  3093  uniiunlem  3190  abn0m  3393  rabn0m  3395  rabeq0  3397  abeq0  3398  r19.3rmv  3458  r19.28mv  3460  r19.27mv  3464  raaanv  3475  sbss  3476  nfifd  3504  euabsn  3601  oprcl  3737  nfuni  3750  nfunid  3751  eluniab  3756  nfint  3789  elintab  3790  iineq2dv  3843  disjiun  3932  opabbidv  4002  nfopab  4004  cbvopab  4007  cbvopabv  4008  cbvopab1  4009  cbvopab2  4010  cbvopab1s  4011  cbvopab1v  4012  mpteq12f  4016  mpteq2dva  4026  cbvmptf  4030  cbvmpt  4031  zfrep6  4053  zfnuleu  4060  intexabim  4085  iinexgm  4087  repizf2  4094  bnd  4104  copsex2t  4175  copsex2g  4176  opelopabsb  4190  opelopabaf  4203  pofun  4242  frind  4282  reusv3  4389  alxfr  4390  rexxfrd  4392  ralxfrALT  4396  onintonm  4441  sucprcreg  4472  eunex  4484  tfis  4505  tfis2  4507  tfisi  4509  peano2  4517  findes  4525  omsinds  4543  opeliunxp  4602  opeliunxp2  4687  ralxpf  4693  rexxpf  4694  dfdmf  4740  dfrnf  4788  elrnmpt1  4798  intirr  4933  nfiotadw  5099  cbviota  5101  cbviotav  5102  sb8iota  5103  iota2d  5121  iota2  5122  dffun5r  5143  dffun6f  5144  dffun4f  5147  funco  5171  fun11  5198  imadif  5211  isarep1  5217  isarep2  5218  fun11iun  5396  fv3  5452  tz6.12f  5458  tz6.12c  5459  relelfvdm  5461  nfvres  5462  funimass4  5480  funfvdm2f  5494  fvmptss2  5504  fvmptdf  5516  fvmptdv  5517  fvmptt  5520  eqfnfv2f  5530  ralrnmpt  5570  rexrnmpt  5571  f1ompt  5579  ffnfv  5586  ffnfvf  5587  fmptco  5594  elabrex  5667  dff13f  5679  fliftfun  5705  cbvriota  5748  cbvriotav  5749  riota2  5760  riota5f  5762  acexmid  5781  nfoprab  5831  oprabbidv  5833  mpoeq123  5838  cbvoprab1  5851  cbvoprab2  5852  cbvoprab12  5853  cbvoprab12v  5854  cbvoprab3  5855  cbvoprab3v  5856  cbvmpox  5857  ralrnmpo  5893  ovmpodx  5905  ovmpodf  5910  ovmpodv  5911  ovi3  5915  ofrfval2  6006  abrexex2g  6026  opabex3d  6027  opabex3  6028  abrexex2  6030  dfoprab4f  6099  fmpox  6106  spc2ed  6138  cnvoprab  6139  f1od2  6140  opeliunxp2f  6143  tposoprab  6185  nfrecs  6212  tfri3  6272  nffrec  6301  eqerlem  6468  erovlem  6529  mptelixpg  6636  dom2lem  6674  xpf1o  6746  mapxpen  6750  nneneq  6759  findcard2  6791  findcard2s  6792  ac6sfi  6800  fiintim  6825  exmidomni  7022  fodjuomnilemdc  7024  ismkvnex  7037  mkvprop  7040  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  cc3  7100  indpi  7174  prarloclem3step  7328  prmuloc2  7399  ltexprlemm  7432  caucvgprprlemaddq  7540  caucvgsrlemgt1  7627  suplocsrlem  7640  axpre-suploclemres  7733  nn0ind-raph  9192  uzind4s  9412  indstr  9415  supinfneg  9417  infsupneg  9418  lbzbi  9435  fzrevral  9916  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  uzsinds  10246  seq3f1olemstep  10305  seq3f1olemp  10306  fimaxre2  11030  climeu  11097  nfsum1  11157  nfsum  11158  sumrbdclem  11178  summodclem2a  11182  zsumdc  11185  fsum3  11188  isumss  11192  isumss2  11194  fsum3cvg2  11195  fsumsplitf  11209  fsum2dlemstep  11235  fsum00  11263  fsumrelem  11272  mertenslem2  11337  nfcprod1  11355  nfcprod  11356  prodeq2  11358  prodrbdclem  11372  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  divalglemeunn  11654  divalglemeuneg  11656  zsupcllemstep  11674  bezoutlemnewy  11720  bezoutlemmain  11722  bezoutlemzz  11726  bezout  11735  prmind2  11837  oddpwdclemdvds  11884  oddpwdclemndvds  11885  exmidunben  11975  ctiunctlemfo  11988  ctiunct  11989  ctiunctal  11990  cnmpt11  12491  cnmpt21  12499  cnmptcom  12506  imasnopn  12507  mulcncf  12799  ellimc3apf  12837  limccnp2cntop  12854  ch2varv  13146  elab1  13161  elab2a  13162  elabg2  13163  cbvrald  13166  sumdc2  13177  bdsepnft  13256  bdsepnfALT  13258  bj-omssind  13304  bj-bdfindes  13318  bj-nn0suc0  13319  bj-nntrans  13320  bj-nnelirr  13322  bj-omtrans  13325  setindft  13334  bj-inf2vnlem3  13341  bj-inf2vnlem4  13342  bj-nn0sucALT  13347  bj-findis  13348  bj-findes  13350  strcollnft  13353  strcollnfALT  13355  pw1nct  13371  isomninnlem  13400  trilpolemeq1  13408  trirec0  13412  iswomninnlem  13417  ismkvnnlem  13419