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-mp 5  ax-1 6  ax-2 7  ax-3 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  elsb1  2103  elsb2  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  eqsb1lem  2453  eqsb1  2454  clelsb1  2455  clelsb2  2456  abbi  2464  abbidv  2468  cbvabv  2473  clelab  2474  nfcjust  2478  nfcv  2490  nfeqd  2504  nfeld  2505  nfabd2  2508  dvelimdc  2510  cleqf  2514  sbabel  2516  ralbidva  2631  rexbidva  2632  ralbidv  2635  rexbidv  2636  2ralbida  2654  2ralbidva  2655  ralimdva  2693  ralrimiv  2697  r19.21v  2702  ralrimdv  2704  reximdvai  2725  r19.23v  2731  rexlimiv  2733  rexlimdv  2738  r19.37av  2762  r19.41v  2765  reean  2778  reeanv  2779  reubidva  2795  rmobidva  2800  cbvralf  2830  cbvreu  2834  cbvralv  2836  cbvrexv  2837  cbvreuv  2838  cbvrmov  2839  cbvralsv  2847  cbvrexsv  2848  sbralie  2849  cbvrab  2858  cbvrabv  2859  issetf  2865  ceqsalv  2886  ceqsralv  2887  ceqsexv  2895  ceqsex2  2896  ceqsex2v  2897  vtocld  2908  vtocl  2910  vtoclg  2915  vtocl2g  2919  vtoclga  2921  vtocl2gaf  2922  vtocl2ga  2923  vtocl3gaf  2924  vtocl3ga  2925  spcimdv  2937  spcgv  2940  spcegv  2941  rspct  2949  rspc  2950  rspce  2951  rspcv  2952  rspcev  2956  rspc2v  2962  eqvincf  2968  ceqsexgv  2972  elabgt  2983  elab  2986  elabg  2987  elab3g  2992  elrab  2995  ralab2  3002  rexab2  3004  eqeu  3008  mo2icl  3016  mob2  3017  mob  3019  reu2  3025  reu3  3027  sbcco  3069  sbcco2  3070  cbvsbcv  3076  sbcieg  3079  sbcie2g  3080  sbcied  3083  elrabsf  3085  sbcbidv  3101  sbcel2gv  3107  sbcg  3112  sbc2iegf  3113  sbc2ie  3114  rmo2  3132  rmo3  3134  csbeq2dv  3162  nfcsb1d  3167  nfcsbd  3170  csbiebt  3173  csbied  3179  csbie2t  3181  sbcnestg  3186  sbnfc2  3197  cbvralcsf  3199  cbvreucsf  3201  cbvrabcsf  3202  cbvralv2  3203  cbvrexv2  3204  dfss2f  3265  uniiunlem  3354  sbss  3660  nfifd  3686  euabsn  3793  nfuni  3898  nfunid  3899  eluniab  3904  nfint  3937  elintab  3938  iineq2dv  3992  nfiotad  4343  cbviota  4345  cbviotav  4346  sb8iota  4347  iota2d  4367  iota2  4368  ncfinraise  4482  ncfinlower  4484  nfop  4605  copsex2t  4609  copsex2g  4610  opabbidv  4626  nfopab  4628  cbvopab  4631  cbvopabv  4632  cbvopab1  4633  cbvopab2  4634  cbvopab1s  4635  cbvopab1v  4636  opelopabaf  4711  opeliunxp  4821  opeliunxp2  4823  ralxpf  4828  dfdmf  4906  dfrnf  4963  dffun3  5121  dffun6f  5124  fun11  5160  imadif  5172  fun11iun  5306  fv3  5342  tz6.12-1  5345  tz6.12c  5348  funfv2f  5378  eqfnfv2f  5397  ffnfv  5428  ffnfvf  5429  dff13f  5473  nfoprab  5550  oprabbidv  5565  cbvoprab1  5568  cbvoprab2  5569  cbvoprab12  5570  cbvoprab12v  5571  cbvoprab3  5572  cbvoprab3v  5573  ov3  5600  mpteq12f  5656  mpt2eq123  5662  mpteq2dva  5668  cbvmpt  5677  cbvmpt2x  5679  fmpt2x  5731  fvfullfunlem1  5862