ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfv Structured version   GIF version

Theorem nfv 1397
Description: If x is not present in φ, then x is not free in φ. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfv xφ
Distinct variable group:   φ,x

Proof of Theorem nfv
StepHypRef Expression
1 ax-17 1395 . 2 (φxφ)
21nfi 1327 1 xφ
Colors of variables: wff set class
Syntax hints:  wnf 1325
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1314  ax-17 1395
This theorem depends on definitions:  df-bi 110  df-nf 1326
This theorem is referenced by:  nfvd  1398  alexim  1512  19.37aiv  1541  sbiedv  1648  spimv  1668  spimev  1717  19.36aiv  1757  cbval2  1772  cbvex2  1773  cbval2v  1774  cbvex2v  1775  cbvald  1776  cbvaldva  1779  cbvexdva  1780  eeanv  1783  sbco2h  1814  nfsbt  1826  sbnf2  1833  dfsb7a  1846  sbalyz  1851  sbco4lem  1858  sbco4  1859  dvelimALT  1862  eubidv  1884  sb8eu  1889  nfeudv  1891  nfeud  1892  nfeuv  1894  nfeu  1895  mobidv  1912  mo23  1917  sbmo  1935  mo4  1937  moimv  1942  moanimv  1951  bm1.1  2001  eqsb3lem  2116  eqsb3  2117  clelsb3  2118  clelsb4  2119  abbi  2127  abbidv  2131  cbvabv  2137  clelab  2138  nfcjust  2142  nfcv  2154  nfeqd  2168  nfeld  2169  nfabd  2172  dvelimdc  2173  cleqf  2177  sbabel  2179  ralbidva  2294  rexbidva  2295  ralbidv  2298  rexbidv  2299  2ralbida  2317  2ralbidva  2318  nfraldya  2330  nfrexdya  2331  rgen2a  2347  ralimdva  2359  ralrimiv  2363  r19.21v  2368  ralrimdv  2370  reximdvai  2391  r19.23v  2397  rexlimiv  2399  rexlimdv  2404  r19.29af  2425  r19.29a  2426  r19.32vr  2430  r19.37av  2435  r19.41v  2438  reean  2450  reeanv  2451  reubidva  2464  rmobidva  2469  cbvralf  2499  cbvrexf  2500  cbvreu  2503  cbvralv  2505  cbvrexv  2506  cbvreuv  2507  cbvrmov  2508  cbvralsv  2516  cbvrexsv  2517  sbralie  2518  cbvrab  2527  cbvrabv  2528  issetf  2534  ceqsalv  2555  ceqsralv  2556  ceqsexv  2564  ceqsex2  2565  ceqsex2v  2566  vtocld  2577  vtocl  2579  vtocl2  2580  vtocl3  2581  vtoclg  2584  vtocl2g  2588  vtoclga  2590  vtocl2gaf  2591  vtocl2ga  2592  vtocl3gaf  2593  vtocl3ga  2594  spcimdv  2608  spcimedv  2610  spcgv  2611  spcegv  2612  rspct  2620  rspc  2621  rspce  2622  rspcv  2623  rspcev  2627  rspc2v  2633  eqvincg  2639  eqvincf  2640  ceqsexgv  2644  elabgt  2655  elab  2658  elabg  2659  elab3g  2664  elrab3t  2668  elrab  2669  ralab2  2676  rexab2  2678  eqeu  2682  mosubt  2689  mo2icl  2691  mob2  2692  mob  2694  reu2  2700  reu3  2702  nfcdeq  2732  sbcco  2756  sbcco2  2757  cbvsbcv  2763  sbcieg  2766  sbcie2g  2767  sbcied  2770  elrabsf  2772  sbcbidv  2788  sbcg  2798  sbc2iegf  2799  sbc2ie  2800  rmo2ilem  2818  rmo3  2820  csbeq2dv  2846  nfcsb1d  2851  nfcsbd  2854  csbiebt  2857  csbied  2863  csbie2t  2865  sbcnestg  2870  sbnfc2  2877  cbvralcsf  2879  cbvrexcsf  2880  cbvreucsf  2881  cbvrabcsf  2882  cbvralv2  2883  cbvrexv2  2884  dfss2f  2907  uniiunlem  2999  rabn0m  3216  rabeq0  3218  abeq0  3219  r19.3rmv  3283  r19.28mv  3285  r19.27mv  3288  raaanv  3299  sbss  3300  nfifd  3324  euabsn  3406  oprcl  3539  nfuni  3552  nfunid  3553  eluniab  3558  nfint  3591  elintab  3592  iineq2dv  3645  opabbidv  3789  nfopab  3791  cbvopab  3794  cbvopabv  3795  cbvopab1  3796  cbvopab2  3797  cbvopab1s  3798  cbvopab1v  3799  mpteq12f  3803  mpteq2dva  3813  cbvmpt  3817  zfrep6  3840  zfnuleu  3847  intexabim  3872  iinexgm  3874  repizf2  3881  bnd  3891  copsex2t  3948  copsex2g  3949  opelopabsb  3963  opelopabaf  3976  pofun  4015  reusv3  4133  alxfr  4134  rexxfrd  4136  ralxfrALT  4140  sucprcreg  4202  eunex  4214  tfis  4224  tfis2  4226  tfisi  4228  peano2  4236  findes  4244  opeliunxp  4313  opeliunxp2  4394  ralxpf  4400  rexxpf  4401  dfdmf  4446  dfrnf  4493  elrnmpt1  4503  intirr  4629  nfiotadxy  4788  cbviota  4790  cbviotav  4791  sb8iota  4792  iota2d  4810  iota2  4811  dffun6f  4832  dffun4f  4835  funco  4857  fun11  4883  imadif  4896  isarep1  4902  isarep2  4903  fun11iun  5063  fv3  5113  tz6.12f  5118  tz6.12c  5119  relelfvdm  5121  nfvres  5122  funimass4  5140  funfvdm2f  5154  fvmptss2  5163  fvmptdf  5174  fvmptdv  5175  fvmptt  5178  eqfnfv2f  5185  ralrnmpt  5225  rexrnmpt  5226  f1ompt  5236  ffnfv  5239  ffnfvf  5240  fmptco  5246  elabrex  5313  dff13f  5325  fliftfun  5352  cbvriota  5393  cbvriotav  5394  riota2  5405  riota5f  5407  acexmid  5426  nfoprab  5471  oprabbidv  5473  mpt2eq123  5478  cbvoprab1  5490  cbvoprab2  5491  cbvoprab12  5492  cbvoprab12v  5493  cbvoprab3  5494  cbvoprab3v  5495  cbvmpt2x  5496  ralrnmpt2  5529  ovmpt2dx  5541  ovmpt2df  5546  ovmpt2dv  5547  ovi3  5551  ofrfval2  5641  abrexex2g  5661  opabex3d  5662  opabex3  5663  abrexex2  5665  dfoprab4f  5733  fmpt2x  5740  tposoprab  5808  nfrecs  5835  tfri3  5866  eqerlem  6039  erovlem  6100  prarloclem3step  6339  prmuloc2  6400  ltexprlemm  6426  nn0ind-raph  7923  ch2varv  8365  elab1  8379  elab2a  8380  elabg2  8381  cbvrald  8384  bdsepnft  8463  bdsepnfALT  8465  bj-omssind  8511  bj-bdfindes  8525  bj-nn0suc0  8526  bj-nntrans  8527  bj-nnelirr  8529  bj-omtrans  8532  setindft  8537  bj-inf2vnlem3  8544  bj-inf2vnlem4  8545  bj-nn0sucALT  8550  bj-findis  8551  bj-findes  8553  strcollnft  8556  strcollnfALT  8558  sscoll2  8560
  Copyright terms: Public domain W3C validator