Theorem nfcv 2339

Description: If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfcv	|- F/_ x A

Distinct variable group:   x, A

Proof of Theorem nfcv

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1542	. 2 |- F/ x y e. A
2	1	nfci 2329	1 |- F/_ x A

Syntax hints:   e. wcel 2167   F/_wnfc 2326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1463  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-nfc 2328

This theorem is referenced by:  nfcvd  2340  nfel  2348  nfeq1  2349  nfel1  2350  nfeq2  2351  nfel2  2352  nfcvf  2362  r2al  2516  r2ex  2517  nfraldxy  2530  nfrexdxy  2531  nfra2xy  2539  r19.12  2603  ralcom  2660  rexcom  2661  nfreudxy  2671  raleq  2693  rexeq  2694  reueq1  2695  rmoeq1  2696  cbvralw  2723  cbvrexw  2724  cbvral  2725  cbvrex  2726  rabeq  2755  rabeqi  2756  cbvrabv  2762  vtoclg  2824  vtocl2g  2828  vtoclga  2830  vtocl2ga  2832  vtocl3ga  2834  spcimdv  2848  spcimedv  2850  spcgv  2851  spcegv  2852  rspct  2861  rspc  2862  rspce  2863  rspc2  2879  ceqsexg  2892  elabgt  2905  elabf  2907  elabg  2910  elab3g  2915  elrab  2920  mob  2946  nfsbc1v  3008  elrabsf  3028  sbcralt  3066  sbcrext  3067  sbcralg  3068  sbcrex  3069  sbcreug  3070  cbvcsbv  3090  csbconstg  3098  nfcsb1v  3117  csbie  3130  csbnestg  3139  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  cbvralv2  3151  cbvrexv2  3152  dfss4st  3396  n0rf  3463  n0r  3464  eq0  3469  raaanlem  3555  nfpw  3618  cbviunv  3955  cbviinv  3956  ssiun2s  3960  iunab  3963  ssiinf  3966  ssiin  3967  iinab  3978  cbvdisjv  4021  nfdisjv  4022  disjnims  4025  disji2  4026  cbvmptv  4129  triun  4144  csbexga  4161  repizf2  4195  moop2  4284  euotd  4287  opelopabgf  4304  opelopabf  4309  nfpo  4336  nfso  4337  pofun  4347  nfse  4376  nffrfor  4383  nffr  4384  frind  4387  nfwe  4390  eusvnf  4488  rabxfrd  4504  tfis  4619  tfisi  4623  opeliunxp  4718  nfrel  4748  opeliunxp2  4806  ralxpf  4812  rexxpf  4813  nfco  4831  nfcnv  4845  dfdmf  4859  dfrnf  4907  nfdm  4910  nfres  4948  resmptf  4996  nfiotadw  5222  dffun6f  5271  dffun6  5272  dffun4f  5274  nffun  5281  funimaexglem  5341  nffv  5568  nffvmpt1  5569  dffn5imf  5616  funfvdm2f  5626  fvmptss2  5636  fvmpts  5639  fvmpt2  5645  fvmptssdm  5646  mptfvex  5647  fvmptdv  5650  fvmptd3  5655  elfvmptrab1  5656  eqfnfv2f  5663  ralrnmpt  5704  rexrnmpt  5705  f1ompt  5713  ffnfvf  5721  fmptco  5728  fmptcof  5729  fmptcos  5730  funiunfvdmf  5811  dff13f  5817  f1mpt  5818  fliftfuns  5845  nfiso  5853  nfriotadxy  5886  csbriotag  5890  riota2  5900  mpoeq123  5981  cbvmpox  6000  cbvmpo  6001  cbvmpov  6002  ovmpos  6046  ov2gf  6047  ovmpodxf  6048  ovmpodx  6049  ovmpodv  6055  ovmpodv2  6056  fvmpopr2d  6059  ovi3  6060  elovmporab  6123  elovmporab1w  6124  nfof  6141  nfofr  6142  offval2  6151  ofrfval2  6152  abrexex2g  6177  abrexex2  6181  uchoice  6195  dfopab2  6247  dfoprab3s  6248  mpomptsx  6255  dmmpossx  6257  fmpox  6258  mpofvex  6263  fnmpoovd  6273  fmpoco  6274  dfmpo  6281  f1od2  6293  disjxp1  6294  mpoxopoveq  6298  mpoxopovel  6299  nftpos  6337  tposoprab  6338  nfrecs  6365  nffrec  6454  eqerlem  6623  qliftfuns  6678  cbvixpv  6775  nfixpxy  6776  nfixp1  6777  ixpf  6779  mptelixpg  6793  dom2lem  6831  xpcomco  6885  xpf1o  6905  mapxpen  6909  ac6sfi  6959  opabfi  6999  nfsup  7058  nfdju  7108  exmidomni  7208  ismkvnex  7221  cc2  7334  cc4f  7336  cc4  7337  caucvgprprlemaddq  7775  caucvgsrlemgt1  7862  axpre-suploclemres  7968  lble  8974  supinfneg  9669  infsupneg  9670  fzrevral  10180  zsupcllemstep  10319  infssuzex  10323  infssuzcldc  10325  nfseq  10549  seq3f1olemstep  10606  seq3f1olemp  10607  nfwrd  10963  fimaxre2  11392  nfsum1  11521  nfsum  11522  cbvsumv  11526  cbvsumi  11527  sumfct  11539  sumrbdclem  11542  summodclem2a  11546  zsumdc  11549  fsum3  11552  isumss  11556  isumss2  11558  fsum3cvg2  11559  fsumzcl2  11570  fsumadd  11571  fsumsplitf  11573  sumsnf  11574  sumsn  11576  sumsns  11580  fsumsplitsnun  11584  fsum2dlemstep  11599  fisumcom2  11603  fsumshftm  11610  fsum00  11627  fsumrelem  11636  fsumiun  11642  mertenslem2  11701  prodeq1  11718  nfcprod1  11719  nfcprod  11720  cbvprod  11723  cbvprodv  11724  cbvprodi  11725  prodrbdclem  11736  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  fprodntrivap  11749  prodfct  11752  prodssdc  11754  prodsnf  11757  prodsn  11758  fprodm1s  11766  fprodp1s  11767  prodsns  11768  fprodcllemf  11778  fprodconst  11785  fprodap0  11786  fprod2dlemstep  11787  fprodcom2fi  11791  fprodrec  11794  fproddivapf  11796  fprodsplitf  11797  fprodap0f  11801  fprodle  11805  bezoutlemmain  12165  bezout  12178  nnwofdc  12205  nnwosdc  12206  prmind2  12288  oddpwdclemdvds  12338  oddpwdclemndvds  12339  pcmpt  12512  pcmptdvds  12514  ctiunctlemudc  12654  ctiunctlemf  12655  ctiunctlemfo  12656  ctiunct  12657  ctiunctal  12658  gsumfzconstf  13472  cnmpt11  14519  cnmpt1t  14521  cnmpt21  14527  cnmpt2t  14529  cnmptcom  14534  imasnopn  14535  fsumcncntop  14803  ellimc3apf  14896  ellimc3ap  14897  limcmpted  14899  dvmptfsum  14961  elplyd  14977  fsumdvdsmul  15227  lgseisenlem2  15312  elabf1  15427  elabf2  15428  elabg2  15431  bj-omssind  15581  bj-bdfindisg  15594  bj-nntrans  15597  bj-nnelirr  15599  bj-omtrans  15602  setindis  15613  bdsetindis  15615  bj-nn0sucALT  15624  bj-findis  15625  bj-findisg  15626  strcollnfALT  15632  isomninnlem  15674  trilpolemeq1  15684  trirec0  15688  iswomninnlem  15693  ismkvnnlem  15696  nconstwlpolemgt0  15708