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  5639  nffvmpt1  5640  dffn5imf  5691  funfvdm2f  5701  fvmptss2  5711  fvmpts  5714  fvmpt2  5720  fvmptssdm  5721  mptfvex  5722  fvmptdv  5725  fvmptd3  5730  elfvmptrab1  5731  eqfnfv2f  5738  ralrnmpt  5779  rexrnmpt  5780  f1ompt  5788  ffnfvf  5796  fmptco  5803  fmptcof  5804  fmptcos  5805  funiunfvdmf  5894  dff13f  5900  f1mpt  5901  fliftfuns  5928  nfiso  5936  nfriotadxy  5969  csbriotag  5974  riota2  5984  mpoeq123  6069  cbvmpox  6088  cbvmpo  6089  cbvmpov  6090  ovmpos  6134  ov2gf  6135  ovmpodxf  6136  ovmpodx  6137  ovmpodv  6143  ovmpodv2  6144  fvmpopr2d  6147  ovi3  6148  elovmporab  6211  elovmporab1w  6212  nfof  6230  nfofr  6231  offval2  6240  ofrfval2  6241  abrexex2g  6271  abrexex2  6275  uchoice  6289  dfopab2  6341  dfoprab3s  6342  mpomptsx  6349  dmmpossx  6351  fmpox  6352  mpofvex  6357  fnmpoovd  6367  fmpoco  6368  dfmpo  6375  f1od2  6387  disjxp1  6388  mpoxopoveq  6392  mpoxopovel  6393  nftpos  6431  tposoprab  6432  nfrecs  6459  nffrec  6548  eqerlem  6719  qliftfuns  6774  cbvixpv  6871  nfixpxy  6872  nfixp1  6873  ixpf  6875  mptelixpg  6889  dom2lem  6931  xpcomco  6993  xpf1o  7013  mapxpen  7017  ac6sfi  7068  opabfi  7111  nfsup  7170  nfdju  7220  exmidomni  7320  ismkvnex  7333  cc2  7464  cc4f  7466  cc4  7467  caucvgprprlemaddq  7906  caucvgsrlemgt1  7993  axpre-suploclemres  8099  lble  9105  supinfneg  9802  infsupneg  9803  fzrevral  10313  zsupcllemstep  10461  infssuzex  10465  infssuzcldc  10467  nfseq  10691  seq3f1olemstep  10748  seq3f1olemp  10749  nfwrd  11113  reuccatpfxs1v  11296  fimaxre2  11754  nfsum1  11883  nfsum  11884  cbvsumv  11888  cbvsumi  11889  sumfct  11901  sumrbdclem  11904  summodclem2a  11908  zsumdc  11911  fsum3  11914  isumss  11918  isumss2  11920  fsum3cvg2  11921  fsumzcl2  11932  fsumadd  11933  fsumsplitf  11935  sumsnf  11936  sumsn  11938  sumsns  11942  fsumsplitsnun  11946  fsum2dlemstep  11961  fisumcom2  11965  fsumshftm  11972  fsum00  11989  fsumrelem  11998  fsumiun  12004  mertenslem2  12063  prodeq1  12080  nfcprod1  12081  nfcprod  12082  cbvprod  12085  cbvprodv  12086  cbvprodi  12087  prodrbdclem  12098  prodmodclem2a  12103  zproddc  12106  fprodseq  12110  fprodntrivap  12111  prodfct  12114  prodssdc  12116  prodsnf  12119  prodsn  12120  fprodm1s  12128  fprodp1s  12129  prodsns  12130  fprodcllemf  12140  fprodconst  12147  fprodap0  12148  fprod2dlemstep  12149  fprodcom2fi  12153  fprodrec  12156  fproddivapf  12158  fprodsplitf  12159  fprodap0f  12163  fprodle  12167  bezoutlemmain  12535  bezout  12548  nnwofdc  12575  nnwosdc  12576  prmind2  12658  oddpwdclemdvds  12708  oddpwdclemndvds  12709  pcmpt  12882  pcmptdvds  12884  ctiunctlemudc  13024  ctiunctlemf  13025  ctiunctlemfo  13026  ctiunct  13027  ctiunctal  13028  prdsbas3  13336  gsumfzconstf  13895  cnmpt11  14973  cnmpt1t  14975  cnmpt21  14981  cnmpt2t  14983  cnmptcom  14988  imasnopn  14989  fsumcncntop  15257  ellimc3apf  15350  ellimc3ap  15351  limcmpted  15353  dvmptfsum  15415  elplyd  15431  fsumdvdsmul  15681  lgseisenlem2  15766  gropd  15864  grstructd2dom  15865  lfgrnloopen  15947  elabf1  16228  elabf2  16229  elabg2  16232  bj-omssind  16381  bj-bdfindisg  16394  bj-nntrans  16397  bj-nnelirr  16399  bj-omtrans  16402  setindis  16413  bdsetindis  16415  bj-nn0sucALT  16424  bj-findis  16425  bj-findisg  16426  strcollnfALT  16432  isomninnlem  16486  trilpolemeq1  16496  trirec0  16500  iswomninnlem  16505  ismkvnnlem  16508  nconstwlpolemgt0  16520