Theorem nfcv 2372

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 1574	. 2 |- F/ x y e. A
2	1	nfci 2362	1 |- F/_ x A

Syntax hints:   e. wcel 2200   F/_wnfc 2359

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 1495  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-nfc 2361

This theorem is referenced by:  nfcvd  2373  nfel  2381  nfeq1  2382  nfel1  2383  nfeq2  2384  nfel2  2385  nfcvf  2395  r2al  2549  r2ex  2550  nfraldxy  2563  nfrexdxy  2564  nfra2xy  2572  r19.12  2637  ralcom  2694  rexcom  2695  nfreudxy  2705  raleq  2728  rexeq  2729  reueq1  2730  rmoeq1  2731  cbvralw  2758  cbvrexw  2759  cbvral  2761  cbvrex  2762  rabeq  2791  rabeqi  2792  cbvrabv  2798  vtoclg  2861  vtocl2g  2865  vtoclga  2867  vtocl2ga  2869  vtocl3ga  2871  spcimdv  2887  spcimedv  2889  spcgv  2890  spcegv  2891  rspct  2900  rspc  2901  rspce  2902  rspc2  2918  ceqsexg  2931  elabgt  2944  elabf  2946  elabg  2949  elab3g  2954  elrab  2959  mob  2985  nfsbc1v  3047  elrabsf  3067  sbcralt  3105  sbcrext  3106  sbcralg  3107  sbcrex  3108  sbcreug  3109  reu8nf  3110  cbvcsbv  3130  csbconstg  3138  nfcsb1v  3157  csbie  3170  csbnestg  3179  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  cbvralv2  3191  cbvrexv2  3192  dfss4st  3437  n0rf  3504  n0r  3505  eq0  3510  raaanlem  3596  nfpw  3662  cbviunv  4004  cbviinv  4005  ssiun2s  4009  iunab  4012  ssiinf  4015  ssiin  4016  iinab  4027  cbvdisjv  4070  nfdisjv  4071  disjnims  4074  disji2  4075  invdisjrab  4077  cbvmptv  4180  triun  4195  csbexga  4212  repizf2  4246  moop2  4338  euotd  4341  opelopabgf  4358  opelopabf  4363  nfpo  4392  nfso  4393  pofun  4403  nfse  4432  nffrfor  4439  nffr  4440  frind  4443  nfwe  4446  eusvnf  4544  rabxfrd  4560  tfis  4675  tfisi  4679  opeliunxp  4774  nfrel  4804  opeliunxp2  4862  ralxpf  4868  rexxpf  4869  nfco  4887  nfcnv  4901  dfdmf  4916  dfrnf  4965  nfdm  4968  nfres  5007  resmptf  5055  nfiotadw  5281  dffun6f  5331  dffun6  5332  dffun4f  5334  nffun  5341  funimaexglem  5404  nffv  5637  nffvmpt1  5638  dffn5imf  5689  funfvdm2f  5699  fvmptss2  5709  fvmpts  5712  fvmpt2  5718  fvmptssdm  5719  mptfvex  5720  fvmptdv  5723  fvmptd3  5728  elfvmptrab1  5729  eqfnfv2f  5736  ralrnmpt  5777  rexrnmpt  5778  f1ompt  5786  ffnfvf  5794  fmptco  5801  fmptcof  5802  fmptcos  5803  funiunfvdmf  5888  dff13f  5894  f1mpt  5895  fliftfuns  5922  nfiso  5930  nfriotadxy  5963  csbriotag  5968  riota2  5978  mpoeq123  6063  cbvmpox  6082  cbvmpo  6083  cbvmpov  6084  ovmpos  6128  ov2gf  6129  ovmpodxf  6130  ovmpodx  6131  ovmpodv  6137  ovmpodv2  6138  fvmpopr2d  6141  ovi3  6142  elovmporab  6205  elovmporab1w  6206  nfof  6224  nfofr  6225  offval2  6234  ofrfval2  6235  abrexex2g  6265  abrexex2  6269  uchoice  6283  dfopab2  6335  dfoprab3s  6336  mpomptsx  6343  dmmpossx  6345  fmpox  6346  mpofvex  6351  fnmpoovd  6361  fmpoco  6362  dfmpo  6369  f1od2  6381  disjxp1  6382  mpoxopoveq  6386  mpoxopovel  6387  nftpos  6425  tposoprab  6426  nfrecs  6453  nffrec  6542  eqerlem  6711  qliftfuns  6766  cbvixpv  6863  nfixpxy  6864  nfixp1  6865  ixpf  6867  mptelixpg  6881  dom2lem  6923  xpcomco  6985  xpf1o  7005  mapxpen  7009  ac6sfi  7060  opabfi  7100  nfsup  7159  nfdju  7209  exmidomni  7309  ismkvnex  7322  cc2  7453  cc4f  7455  cc4  7456  caucvgprprlemaddq  7895  caucvgsrlemgt1  7982  axpre-suploclemres  8088  lble  9094  supinfneg  9790  infsupneg  9791  fzrevral  10301  zsupcllemstep  10449  infssuzex  10453  infssuzcldc  10455  nfseq  10679  seq3f1olemstep  10736  seq3f1olemp  10737  nfwrd  11100  reuccatpfxs1v  11280  fimaxre2  11738  nfsum1  11867  nfsum  11868  cbvsumv  11872  cbvsumi  11873  sumfct  11885  sumrbdclem  11888  summodclem2a  11892  zsumdc  11895  fsum3  11898  isumss  11902  isumss2  11904  fsum3cvg2  11905  fsumzcl2  11916  fsumadd  11917  fsumsplitf  11919  sumsnf  11920  sumsn  11922  sumsns  11926  fsumsplitsnun  11930  fsum2dlemstep  11945  fisumcom2  11949  fsumshftm  11956  fsum00  11973  fsumrelem  11982  fsumiun  11988  mertenslem2  12047  prodeq1  12064  nfcprod1  12065  nfcprod  12066  cbvprod  12069  cbvprodv  12070  cbvprodi  12071  prodrbdclem  12082  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  fprodntrivap  12095  prodfct  12098  prodssdc  12100  prodsnf  12103  prodsn  12104  fprodm1s  12112  fprodp1s  12113  prodsns  12114  fprodcllemf  12124  fprodconst  12131  fprodap0  12132  fprod2dlemstep  12133  fprodcom2fi  12137  fprodrec  12140  fproddivapf  12142  fprodsplitf  12143  fprodap0f  12147  fprodle  12151  bezoutlemmain  12519  bezout  12532  nnwofdc  12559  nnwosdc  12560  prmind2  12642  oddpwdclemdvds  12692  oddpwdclemndvds  12693  pcmpt  12866  pcmptdvds  12868  ctiunctlemudc  13008  ctiunctlemf  13009  ctiunctlemfo  13010  ctiunct  13011  ctiunctal  13012  prdsbas3  13320  gsumfzconstf  13879  cnmpt11  14957  cnmpt1t  14959  cnmpt21  14965  cnmpt2t  14967  cnmptcom  14972  imasnopn  14973  fsumcncntop  15241  ellimc3apf  15334  ellimc3ap  15335  limcmpted  15337  dvmptfsum  15399  elplyd  15415  fsumdvdsmul  15665  lgseisenlem2  15750  gropd  15848  grstructd2dom  15849  lfgrnloopen  15931  elabf1  16145  elabf2  16146  elabg2  16149  bj-omssind  16298  bj-bdfindisg  16311  bj-nntrans  16314  bj-nnelirr  16316  bj-omtrans  16319  setindis  16330  bdsetindis  16332  bj-nn0sucALT  16341  bj-findis  16342  bj-findisg  16343  strcollnfALT  16349  isomninnlem  16398  trilpolemeq1  16408  trirec0  16412  iswomninnlem  16417  ismkvnnlem  16420  nconstwlpolemgt0  16432