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

Theorem nfv 1508
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
StepHypRef Expression
1 ax-17 1506 . 2  |-  ( ph  ->  A. x ph )
21nfi 1438 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1436
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 1425  ax-17 1506
This theorem depends on definitions:  df-bi 116  df-nf 1437
This theorem is referenced by:  nfvd  1509  alexim  1624  19.37aiv  1653  sbiedv  1762  spimv  1783  spimev  1833  19.36aiv  1873  cbval2  1893  cbvex2  1894  cbval2v  1895  cbvex2v  1896  cbvald  1897  cbvaldva  1900  cbvexdva  1901  eeanv  1904  sbco2h  1937  nfsbt  1949  sbnf2  1956  dfsb7a  1969  sbalyz  1974  sbco4lem  1981  sbco4  1982  dvelimALT  1985  eubidv  2007  sb8eu  2012  nfeudv  2014  nfeud  2015  nfeuv  2017  nfeu  2018  mobidv  2035  mo23  2040  sbmo  2058  mo4  2060  moimv  2065  moanimv  2074  bm1.1  2124  eqsb3lem  2242  eqsb3  2243  clelsb3  2244  clelsb4  2245  abbi  2253  abbidv  2257  cbvabv  2264  clelab  2265  nfcjust  2269  nfcv  2281  clelsb3f  2285  nfeqd  2296  nfeld  2297  nfabd  2300  dvelimdc  2301  cleqf  2305  sbabel  2307  ralbidva  2433  rexbidva  2434  ralbidv  2437  rexbidv  2438  2ralbida  2456  2ralbidva  2457  nfraldya  2469  nfrexdya  2470  rgen2a  2486  ralimdva  2499  ralrimiv  2504  r19.21v  2509  ralrimdv  2511  reximdvai  2532  r19.23v  2541  rexlimiv  2543  rexlimdv  2548  r19.29af  2573  r19.29an  2574  r19.29a  2575  r19.32vr  2579  r19.37av  2584  r19.41v  2587  reean  2599  reeanv  2600  reubidva  2613  rmobidva  2618  cbvralf  2648  cbvrexf  2649  cbvreu  2652  cbvralv  2654  cbvrexv  2655  cbvreuv  2656  cbvrmov  2657  cbvralsv  2668  cbvrexsv  2669  sbralie  2670  cbvrab  2684  cbvrabv  2685  issetf  2693  ceqsalv  2716  ceqsralv  2717  ceqsexv  2725  ceqsex2  2726  ceqsex2v  2727  vtocld  2738  vtocl  2740  vtocl2  2741  vtocl3  2742  vtoclg  2746  vtocl2g  2750  vtoclga  2752  vtocl2gaf  2753  vtocl2ga  2754  vtocl3gaf  2755  vtocl3ga  2756  spcimdv  2770  spcimedv  2772  spcgv  2773  spcegv  2774  rspct  2782  rspc  2783  rspce  2784  rspcv  2785  rspcev  2789  rspc2v  2802  eqvincg  2809  eqvincf  2810  ceqsexgv  2814  elabgt  2825  elab  2828  elabg  2830  elab3g  2835  elrab3t  2839  elrab  2840  ralab2  2848  rexab2  2850  eqeu  2854  mosubt  2861  mo2icl  2863  mob2  2864  mob  2866  reu2  2872  reu3  2874  rmo4f  2882  nfcdeq  2906  sbcco  2930  sbcco2  2931  cbvsbcv  2938  sbcieg  2941  sbcie2g  2942  sbcied  2945  elrabsf  2947  sbcbidv  2967  sbcg  2978  sbc2iegf  2979  sbc2ie  2980  rmo2ilem  2998  rmo3  3000  csbeq2dv  3028  nfcsb1d  3033  nfcsbd  3036  csbiebt  3039  csbied  3046  csbie2t  3048  sbcnestg  3053  sbnfc2  3060  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  cbvralv2  3066  cbvrexv2  3067  dfss2f  3088  uniiunlem  3185  abn0m  3388  rabn0m  3390  rabeq0  3392  abeq0  3393  r19.3rmv  3453  r19.28mv  3455  r19.27mv  3459  raaanv  3470  sbss  3471  nfifd  3499  euabsn  3593  oprcl  3729  nfuni  3742  nfunid  3743  eluniab  3748  nfint  3781  elintab  3782  iineq2dv  3835  disjiun  3924  opabbidv  3994  nfopab  3996  cbvopab  3999  cbvopabv  4000  cbvopab1  4001  cbvopab2  4002  cbvopab1s  4003  cbvopab1v  4004  mpteq12f  4008  mpteq2dva  4018  cbvmptf  4022  cbvmpt  4023  zfrep6  4045  zfnuleu  4052  intexabim  4077  iinexgm  4079  repizf2  4086  bnd  4096  copsex2t  4167  copsex2g  4168  opelopabsb  4182  opelopabaf  4195  pofun  4234  frind  4274  reusv3  4381  alxfr  4382  rexxfrd  4384  ralxfrALT  4388  onintonm  4433  sucprcreg  4464  eunex  4476  tfis  4497  tfis2  4499  tfisi  4501  peano2  4509  findes  4517  omsinds  4535  opeliunxp  4594  opeliunxp2  4679  ralxpf  4685  rexxpf  4686  dfdmf  4732  dfrnf  4780  elrnmpt1  4790  intirr  4925  nfiotadw  5091  cbviota  5093  cbviotav  5094  sb8iota  5095  iota2d  5113  iota2  5114  dffun5r  5135  dffun6f  5136  dffun4f  5139  funco  5163  fun11  5190  imadif  5203  isarep1  5209  isarep2  5210  fun11iun  5388  fv3  5444  tz6.12f  5450  tz6.12c  5451  relelfvdm  5453  nfvres  5454  funimass4  5472  funfvdm2f  5486  fvmptss2  5496  fvmptdf  5508  fvmptdv  5509  fvmptt  5512  eqfnfv2f  5522  ralrnmpt  5562  rexrnmpt  5563  f1ompt  5571  ffnfv  5578  ffnfvf  5579  fmptco  5586  elabrex  5659  dff13f  5671  fliftfun  5697  cbvriota  5740  cbvriotav  5741  riota2  5752  riota5f  5754  acexmid  5773  nfoprab  5823  oprabbidv  5825  mpoeq123  5830  cbvoprab1  5843  cbvoprab2  5844  cbvoprab12  5845  cbvoprab12v  5846  cbvoprab3  5847  cbvoprab3v  5848  cbvmpox  5849  ralrnmpo  5885  ovmpodx  5897  ovmpodf  5902  ovmpodv  5903  ovi3  5907  ofrfval2  5998  abrexex2g  6018  opabex3d  6019  opabex3  6020  abrexex2  6022  dfoprab4f  6091  fmpox  6098  spc2ed  6130  cnvoprab  6131  f1od2  6132  opeliunxp2f  6135  tposoprab  6177  nfrecs  6204  tfri3  6264  nffrec  6293  eqerlem  6460  erovlem  6521  mptelixpg  6628  dom2lem  6666  xpf1o  6738  mapxpen  6742  nneneq  6751  findcard2  6783  findcard2s  6784  ac6sfi  6792  fiintim  6817  exmidomni  7014  fodjuomnilemdc  7016  ismkvnex  7029  mkvprop  7032  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  cc3  7083  indpi  7157  prarloclem3step  7311  prmuloc2  7382  ltexprlemm  7415  caucvgprprlemaddq  7523  caucvgsrlemgt1  7610  suplocsrlem  7623  axpre-suploclemres  7716  nn0ind-raph  9175  uzind4s  9392  indstr  9395  supinfneg  9397  infsupneg  9398  lbzbi  9415  fzrevral  9892  frecuzrdgtcl  10192  frecuzrdgfunlem  10199  uzsinds  10222  seq3f1olemstep  10281  seq3f1olemp  10282  fimaxre2  11005  climeu  11072  nfsum1  11132  nfsum  11133  sumrbdclem  11153  summodclem2a  11157  zsumdc  11160  fsum3  11163  isumss  11167  isumss2  11169  fsum3cvg2  11170  fsumsplitf  11184  fsum2dlemstep  11210  fsum00  11238  fsumrelem  11247  mertenslem2  11312  nfcprod1  11330  nfcprod  11331  prodeq2  11333  prodrbdclem  11347  prodmodclem2a  11352  divalglemeunn  11625  divalglemeuneg  11627  zsupcllemstep  11645  bezoutlemnewy  11691  bezoutlemmain  11693  bezoutlemzz  11697  bezout  11706  prmind2  11808  oddpwdclemdvds  11855  oddpwdclemndvds  11856  exmidunben  11946  ctiunctlemfo  11959  ctiunct  11960  ctiunctal  11961  cnmpt11  12462  cnmpt21  12470  cnmptcom  12477  imasnopn  12478  mulcncf  12770  ellimc3apf  12808  limccnp2cntop  12825  ch2varv  13005  elab1  13020  elab2a  13021  elabg2  13022  cbvrald  13025  sumdc2  13036  bdsepnft  13115  bdsepnfALT  13117  bj-omssind  13163  bj-bdfindes  13177  bj-nn0suc0  13178  bj-nntrans  13179  bj-nnelirr  13181  bj-omtrans  13184  setindft  13193  bj-inf2vnlem3  13200  bj-inf2vnlem4  13201  bj-nn0sucALT  13206  bj-findis  13207  bj-findes  13209  strcollnft  13212  strcollnfALT  13214  sscoll2  13216  isomninnlem  13255  trilpolemeq1  13263
  Copyright terms: Public domain W3C validator