Theorem nfcv 2374

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

Syntax hints:   e. wcel 2202   F/_wnfc 2361

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 1497  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-nfc 2363

This theorem is referenced by:  nfcvd  2375  nfel  2383  nfeq1  2384  nfel1  2385  nfeq2  2386  nfel2  2387  nfcvf  2397  r2al  2551  r2ex  2552  nfraldxy  2565  nfrexdxy  2566  nfra2xy  2574  r19.12  2639  ralcom  2696  rexcom  2697  nfreudxy  2707  raleq  2730  rexeq  2731  reueq1  2732  rmoeq1  2733  cbvralw  2760  cbvrexw  2761  cbvral  2763  cbvrex  2764  rabeq  2794  rabeqi  2795  cbvrabv  2801  vtoclg  2864  vtocl2g  2868  vtoclga  2870  vtocl2ga  2872  vtocl3ga  2874  spcimdv  2890  spcimedv  2892  spcgv  2893  spcegv  2894  rspct  2903  rspc  2904  rspce  2905  rspc2  2921  ceqsexg  2934  elabgt  2947  elabf  2949  elabg  2952  elab3g  2957  elrab  2962  mob  2988  nfsbc1v  3050  elrabsf  3070  sbcralt  3108  sbcrext  3109  sbcralg  3110  sbcrex  3111  sbcreug  3112  reu8nf  3113  cbvcsbv  3133  csbconstg  3141  nfcsb1v  3160  csbie  3173  csbnestg  3182  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  cbvralv2  3194  cbvrexv2  3195  dfss4st  3440  n0rf  3507  n0r  3508  eq0  3513  raaanlem  3599  nfpw  3665  cbviunv  4009  cbviinv  4010  ssiun2s  4014  iunab  4017  ssiinf  4020  ssiin  4021  iinab  4032  cbvdisjv  4075  nfdisjv  4076  disjnims  4079  disji2  4080  invdisjrab  4082  cbvmptv  4185  triun  4200  csbexga  4217  repizf2  4252  moop2  4344  euotd  4347  opelopabgf  4364  opelopabf  4369  nfpo  4398  nfso  4399  pofun  4409  nfse  4438  nffrfor  4445  nffr  4446  frind  4449  nfwe  4452  eusvnf  4550  rabxfrd  4566  tfis  4681  tfisi  4685  opeliunxp  4781  nfrel  4811  opeliunxp2  4870  ralxpf  4876  rexxpf  4877  nfco  4895  nfcnv  4909  dfdmf  4924  dfrnf  4973  nfdm  4976  nfres  5015  resmptf  5063  nfiotadw  5289  dffun6f  5339  dffun6  5340  dffun4f  5342  nffun  5349  funimaexglem  5413  nffv  5649  nffvmpt1  5650  dffn5imf  5701  funfvdm2f  5711  fvmptss2  5721  fvmpts  5724  fvmpt2  5730  fvmptssdm  5731  mptfvex  5732  fvmptdv  5735  fvmptd3  5740  elfvmptrab1  5741  eqfnfv2f  5748  ralrnmpt  5789  rexrnmpt  5790  f1ompt  5798  ffnfvf  5806  fmptco  5813  fmptcof  5814  fmptcos  5815  funiunfvdmf  5905  dff13f  5911  f1mpt  5912  fliftfuns  5939  nfiso  5947  nfriotadxy  5980  csbriotag  5985  riota2  5995  mpoeq123  6080  cbvmpox  6099  cbvmpo  6100  cbvmpov  6101  ovmpos  6145  ov2gf  6146  ovmpodxf  6147  ovmpodx  6148  ovmpodv  6154  ovmpodv2  6155  fvmpopr2d  6158  ovi3  6159  elovmporab  6222  elovmporab1w  6223  nfof  6241  nfofr  6242  offval2  6251  ofrfval2  6252  abrexex2g  6282  abrexex2  6286  uchoice  6300  dfopab2  6352  dfoprab3s  6353  mpomptsx  6362  dmmpossx  6364  fmpox  6365  mpofvex  6370  fnmpoovd  6380  fmpoco  6381  dfmpo  6388  f1od2  6400  disjxp1  6401  mpoxopoveq  6406  mpoxopovel  6407  nftpos  6445  tposoprab  6446  nfrecs  6473  nffrec  6562  eqerlem  6733  qliftfuns  6788  cbvixpv  6885  nfixpxy  6886  nfixp1  6887  ixpf  6889  mptelixpg  6903  dom2lem  6945  modom  6994  xpcomco  7010  xpf1o  7030  mapxpen  7034  ac6sfi  7087  opabfi  7132  nfsup  7191  nfdju  7241  exmidomni  7341  ismkvnex  7354  cc2  7486  cc4f  7488  cc4  7489  caucvgprprlemaddq  7928  caucvgsrlemgt1  8015  axpre-suploclemres  8121  lble  9127  supinfneg  9829  infsupneg  9830  fzrevral  10340  zsupcllemstep  10490  infssuzex  10494  infssuzcldc  10496  nfseq  10720  seq3f1olemstep  10777  seq3f1olemp  10778  nfwrd  11146  reuccatpfxs1v  11333  fimaxre2  11805  nfsum1  11934  nfsum  11935  cbvsumv  11939  cbvsumi  11940  sumfct  11952  sumrbdclem  11956  summodclem2a  11960  zsumdc  11963  fsum3  11966  isumss  11970  isumss2  11972  fsum3cvg2  11973  fsumzcl2  11984  fsumadd  11985  fsumsplitf  11987  sumsnf  11988  sumsn  11990  sumsns  11994  fsumsplitsnun  11998  fsum2dlemstep  12013  fisumcom2  12017  fsumshftm  12024  fsum00  12041  fsumrelem  12050  fsumiun  12056  mertenslem2  12115  prodeq1  12132  nfcprod1  12133  nfcprod  12134  cbvprod  12137  cbvprodv  12138  cbvprodi  12139  prodrbdclem  12150  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  fprodntrivap  12163  prodfct  12166  prodssdc  12168  prodsnf  12171  prodsn  12172  fprodm1s  12180  fprodp1s  12181  prodsns  12182  fprodcllemf  12192  fprodconst  12199  fprodap0  12200  fprod2dlemstep  12201  fprodcom2fi  12205  fprodrec  12208  fproddivapf  12210  fprodsplitf  12211  fprodap0f  12215  fprodle  12219  bezoutlemmain  12587  bezout  12600  nnwofdc  12627  nnwosdc  12628  prmind2  12710  oddpwdclemdvds  12760  oddpwdclemndvds  12761  pcmpt  12934  pcmptdvds  12936  ctiunctlemudc  13076  ctiunctlemf  13077  ctiunctlemfo  13078  ctiunct  13079  ctiunctal  13080  prdsbas3  13388  gsumfzconstf  13947  gsumsplit0  13951  cnmpt11  15026  cnmpt1t  15028  cnmpt21  15034  cnmpt2t  15036  cnmptcom  15041  imasnopn  15042  fsumcncntop  15310  ellimc3apf  15403  ellimc3ap  15404  limcmpted  15406  dvmptfsum  15468  elplyd  15484  fsumdvdsmul  15734  lgseisenlem2  15819  gropd  15917  grstructd2dom  15918  lfgrnloopen  16003  elabf1  16428  elabf2  16429  elabg2  16432  bj-omssind  16581  bj-bdfindisg  16594  bj-nntrans  16597  bj-nnelirr  16599  bj-omtrans  16602  setindis  16613  bdsetindis  16615  bj-nn0sucALT  16624  bj-findis  16625  bj-findisg  16626  strcollnfALT  16632  isomninnlem  16685  trilpolemeq1  16695  trirec0  16699  iswomninnlem  16705  ismkvnnlem  16708  nconstwlpolemgt0  16720  gfsumsn  16737