Theorem nfcv 2350

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

Syntax hints:   e. wcel 2178   F/_wnfc 2337

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 1473  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-nfc 2339

This theorem is referenced by:  nfcvd  2351  nfel  2359  nfeq1  2360  nfel1  2361  nfeq2  2362  nfel2  2363  nfcvf  2373  r2al  2527  r2ex  2528  nfraldxy  2541  nfrexdxy  2542  nfra2xy  2550  r19.12  2614  ralcom  2671  rexcom  2672  nfreudxy  2682  raleq  2705  rexeq  2706  reueq1  2707  rmoeq1  2708  cbvralw  2735  cbvrexw  2736  cbvral  2738  cbvrex  2739  rabeq  2768  rabeqi  2769  cbvrabv  2775  vtoclg  2838  vtocl2g  2842  vtoclga  2844  vtocl2ga  2846  vtocl3ga  2848  spcimdv  2864  spcimedv  2866  spcgv  2867  spcegv  2868  rspct  2877  rspc  2878  rspce  2879  rspc2  2895  ceqsexg  2908  elabgt  2921  elabf  2923  elabg  2926  elab3g  2931  elrab  2936  mob  2962  nfsbc1v  3024  elrabsf  3044  sbcralt  3082  sbcrext  3083  sbcralg  3084  sbcrex  3085  sbcreug  3086  reu8nf  3087  cbvcsbv  3107  csbconstg  3115  nfcsb1v  3134  csbie  3147  csbnestg  3156  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  cbvralv2  3168  cbvrexv2  3169  dfss4st  3414  n0rf  3481  n0r  3482  eq0  3487  raaanlem  3573  nfpw  3639  cbviunv  3980  cbviinv  3981  ssiun2s  3985  iunab  3988  ssiinf  3991  ssiin  3992  iinab  4003  cbvdisjv  4046  nfdisjv  4047  disjnims  4050  disji2  4051  invdisjrab  4053  cbvmptv  4156  triun  4171  csbexga  4188  repizf2  4222  moop2  4314  euotd  4317  opelopabgf  4334  opelopabf  4339  nfpo  4366  nfso  4367  pofun  4377  nfse  4406  nffrfor  4413  nffr  4414  frind  4417  nfwe  4420  eusvnf  4518  rabxfrd  4534  tfis  4649  tfisi  4653  opeliunxp  4748  nfrel  4778  opeliunxp2  4836  ralxpf  4842  rexxpf  4843  nfco  4861  nfcnv  4875  dfdmf  4890  dfrnf  4938  nfdm  4941  nfres  4980  resmptf  5028  nfiotadw  5254  dffun6f  5303  dffun6  5304  dffun4f  5306  nffun  5313  funimaexglem  5376  nffv  5609  nffvmpt1  5610  dffn5imf  5657  funfvdm2f  5667  fvmptss2  5677  fvmpts  5680  fvmpt2  5686  fvmptssdm  5687  mptfvex  5688  fvmptdv  5691  fvmptd3  5696  elfvmptrab1  5697  eqfnfv2f  5704  ralrnmpt  5745  rexrnmpt  5746  f1ompt  5754  ffnfvf  5762  fmptco  5769  fmptcof  5770  fmptcos  5771  funiunfvdmf  5856  dff13f  5862  f1mpt  5863  fliftfuns  5890  nfiso  5898  nfriotadxy  5931  csbriotag  5935  riota2  5945  mpoeq123  6027  cbvmpox  6046  cbvmpo  6047  cbvmpov  6048  ovmpos  6092  ov2gf  6093  ovmpodxf  6094  ovmpodx  6095  ovmpodv  6101  ovmpodv2  6102  fvmpopr2d  6105  ovi3  6106  elovmporab  6169  elovmporab1w  6170  nfof  6187  nfofr  6188  offval2  6197  ofrfval2  6198  abrexex2g  6228  abrexex2  6232  uchoice  6246  dfopab2  6298  dfoprab3s  6299  mpomptsx  6306  dmmpossx  6308  fmpox  6309  mpofvex  6314  fnmpoovd  6324  fmpoco  6325  dfmpo  6332  f1od2  6344  disjxp1  6345  mpoxopoveq  6349  mpoxopovel  6350  nftpos  6388  tposoprab  6389  nfrecs  6416  nffrec  6505  eqerlem  6674  qliftfuns  6729  cbvixpv  6826  nfixpxy  6827  nfixp1  6828  ixpf  6830  mptelixpg  6844  dom2lem  6886  xpcomco  6946  xpf1o  6966  mapxpen  6970  ac6sfi  7021  opabfi  7061  nfsup  7120  nfdju  7170  exmidomni  7270  ismkvnex  7283  cc2  7414  cc4f  7416  cc4  7417  caucvgprprlemaddq  7856  caucvgsrlemgt1  7943  axpre-suploclemres  8049  lble  9055  supinfneg  9751  infsupneg  9752  fzrevral  10262  zsupcllemstep  10409  infssuzex  10413  infssuzcldc  10415  nfseq  10639  seq3f1olemstep  10696  seq3f1olemp  10697  nfwrd  11059  reuccatpfxs1v  11239  fimaxre2  11653  nfsum1  11782  nfsum  11783  cbvsumv  11787  cbvsumi  11788  sumfct  11800  sumrbdclem  11803  summodclem2a  11807  zsumdc  11810  fsum3  11813  isumss  11817  isumss2  11819  fsum3cvg2  11820  fsumzcl2  11831  fsumadd  11832  fsumsplitf  11834  sumsnf  11835  sumsn  11837  sumsns  11841  fsumsplitsnun  11845  fsum2dlemstep  11860  fisumcom2  11864  fsumshftm  11871  fsum00  11888  fsumrelem  11897  fsumiun  11903  mertenslem2  11962  prodeq1  11979  nfcprod1  11980  nfcprod  11981  cbvprod  11984  cbvprodv  11985  cbvprodi  11986  prodrbdclem  11997  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  fprodntrivap  12010  prodfct  12013  prodssdc  12015  prodsnf  12018  prodsn  12019  fprodm1s  12027  fprodp1s  12028  prodsns  12029  fprodcllemf  12039  fprodconst  12046  fprodap0  12047  fprod2dlemstep  12048  fprodcom2fi  12052  fprodrec  12055  fproddivapf  12057  fprodsplitf  12058  fprodap0f  12062  fprodle  12066  bezoutlemmain  12434  bezout  12447  nnwofdc  12474  nnwosdc  12475  prmind2  12557  oddpwdclemdvds  12607  oddpwdclemndvds  12608  pcmpt  12781  pcmptdvds  12783  ctiunctlemudc  12923  ctiunctlemf  12924  ctiunctlemfo  12925  ctiunct  12926  ctiunctal  12927  prdsbas3  13234  gsumfzconstf  13793  cnmpt11  14870  cnmpt1t  14872  cnmpt21  14878  cnmpt2t  14880  cnmptcom  14885  imasnopn  14886  fsumcncntop  15154  ellimc3apf  15247  ellimc3ap  15248  limcmpted  15250  dvmptfsum  15312  elplyd  15328  fsumdvdsmul  15578  lgseisenlem2  15663  gropd  15761  grstructd2dom  15762  lfgrnloopen  15839  elabf1  15917  elabf2  15918  elabg2  15921  bj-omssind  16070  bj-bdfindisg  16083  bj-nntrans  16086  bj-nnelirr  16088  bj-omtrans  16091  setindis  16102  bdsetindis  16104  bj-nn0sucALT  16113  bj-findis  16114  bj-findisg  16115  strcollnfALT  16121  isomninnlem  16171  trilpolemeq1  16181  trirec0  16185  iswomninnlem  16190  ismkvnnlem  16193  nconstwlpolemgt0  16205