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/xph

Distinct variable group:   ph,x

Proof of Theorem nfv

Step	Hyp	Ref	Expression
1		ax-17 1616	. 2 |- (ph -> A.xph)
2	1	nfi 1551	1 |- F/xph

Syntax hints:   F/wnf 1544

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

This theorem is referenced by:  nfvd  1620  19.21v  1890  19.23v  1891  pm11.53  1893  19.27v  1894  19.28v  1895  19.36v  1896  19.36aiv  1897  19.12vv  1898  19.37v  1899  19.41v  1901  19.42v  1905  eeanv  1913  nexdv  1916  spimv  1990  spimev  1999  cbvalv  2002  cbvexv  2003  cbval2  2004  cbvex2  2005  cbval2v  2006  cbvex2v  2007  cbvaldva  2010  cbvexdva  2011  cleljustALT  2015  dvelimnf  2017  sbiedv  2037  ax16i  2046  ax16ALT2  2048  equsb3lem  2101  equsb3  2102  elsb3  2103  elsb4  2104  sbhb  2107  sbnf2  2108  dfsb7  2119  sbid2v  2123  exsb  2130  exsbOLD  2131  euf  2210  eubidv  2212  nfeud2  2216  sb8eu  2222  mo  2226  euex  2227  euorv  2232  sbmo  2234  mo4f  2236  mo4  2237  mobidv  2239  eu5  2242  moim  2250  morimv  2252  moanim  2260  moanimv  2262  euanv  2265  mopick  2266  moexexv  2274  2mo  2282  2mos  2283  2eu4  2287  2eu6  2289  bm1.1  2338  eqsb3lem  2453  eqsb3  2454  clelsb3  2455  abbi  2463  abbidv  2467  cbvabv  2472  clelab  2473  nfcjust  2477  nfcv  2489  nfeqd  2503  nfeld  2504  nfabd2  2507  dvelimdc  2509  cleqf  2513  sbabel  2515  ralbidva  2630  rexbidva  2631  ralbidv  2634  rexbidv  2635  2ralbida  2653  2ralbidva  2654  ralimdva  2692  ralrimiv  2696  r19.21v  2701  ralrimdv  2703  reximdvai  2724  r19.23v  2730  rexlimiv  2732  rexlimdv  2737  r19.37av  2761  r19.41v  2764  reean  2777  reeanv  2778  reubidva  2794  rmobidva  2799  cbvralf  2829  cbvreu  2833  cbvralv  2835  cbvrexv  2836  cbvreuv  2837  cbvrmov  2838  cbvralsv  2846  cbvrexsv  2847  sbralie  2848  cbvrab  2857  cbvrabv  2858  issetf  2864  ceqsalv  2885  ceqsralv  2886  ceqsexv  2894  ceqsex2  2895  ceqsex2v  2896  vtocld  2907  vtocl  2909  vtoclg  2914  vtocl2g  2918  vtoclga  2920  vtocl2gaf  2921  vtocl2ga  2922  vtocl3gaf  2923  vtocl3ga  2924  spcimdv  2936  spcgv  2939  spcegv  2940  rspct  2948  rspc  2949  rspce  2950  rspcv  2951  rspcev  2955  rspc2v  2961  eqvincf  2967  ceqsexgv  2971  elabgt  2982  elab  2985  elabg  2986  elab3g  2991  elrab  2994  ralab2  3001  rexab2  3003  eqeu  3007  mo2icl  3015  mob2  3016  mob  3018  reu2  3024  reu3  3026  sbcco  3068  sbcco2  3069  cbvsbcv  3075  sbcieg  3078  sbcie2g  3079  sbcied  3082  elrabsf  3084  sbcbidv  3100  sbcel2gv  3106  sbcg  3111  sbc2iegf  3112  sbc2ie  3113  rmo2  3131  rmo3  3133  csbeq2dv  3161  nfcsb1d  3166  nfcsbd  3169  csbiebt  3172  csbied  3178  csbie2t  3180  sbcnestg  3185  sbnfc2  3196  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201  cbvralv2  3202  cbvrexv2  3203  dfss2f  3264  uniiunlem  3353  sbss  3659  nfifd  3685  euabsn  3792  nfuni  3897  nfunid  3898  eluniab  3903  nfint  3936  elintab  3937  iineq2dv  3991  nfiotad  4342  cbviota  4344  cbviotav  4345  sb8iota  4346  iota2d  4366  iota2  4367  ncfinraise  4481  ncfinlower  4483  nfop  4604  copsex2t  4608  copsex2g  4609  opabbidv  4625  nfopab  4627  cbvopab  4630  cbvopabv  4631  cbvopab1  4632  cbvopab2  4633  cbvopab1s  4634  cbvopab1v  4635  opelopabaf  4710  opeliunxp  4820  opeliunxp2  4822  ralxpf  4827  dfdmf  4905  dfrnf  4962  dffun3  5120  dffun6f  5123  fun11  5159  imadif  5171  fun11iun  5305  fv3  5341  tz6.12-1  5344  tz6.12c  5347  funfv2f  5377  eqfnfv2f  5396  ffnfv  5427  ffnfvf  5428  dff13f  5472  nfoprab  5549  oprabbidv  5564  cbvoprab1  5567  cbvoprab2  5568  cbvoprab12  5569  cbvoprab12v  5570  cbvoprab3  5571  cbvoprab3v  5572  ov3  5599  mpteq12f  5655  mpt2eq123  5661  mpteq2dva  5667  cbvmpt  5676  cbvmpt2x  5678  fmpt2x  5730  fvfullfunlem1  5861