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  3397  n0rf  3464  n0r  3465  eq0  3470  raaanlem  3556  nfpw  3619  cbviunv  3956  cbviinv  3957  ssiun2s  3961  iunab  3964  ssiinf  3967  ssiin  3968  iinab  3979  cbvdisjv  4022  nfdisjv  4023  disjnims  4026  disji2  4027  cbvmptv  4130  triun  4145  csbexga  4162  repizf2  4196  moop2  4285  euotd  4288  opelopabgf  4305  opelopabf  4310  nfpo  4337  nfso  4338  pofun  4348  nfse  4377  nffrfor  4384  nffr  4385  frind  4388  nfwe  4391  eusvnf  4489  rabxfrd  4505  tfis  4620  tfisi  4624  opeliunxp  4719  nfrel  4749  opeliunxp2  4807  ralxpf  4813  rexxpf  4814  nfco  4832  nfcnv  4846  dfdmf  4860  dfrnf  4908  nfdm  4911  nfres  4949  resmptf  4997  nfiotadw  5223  dffun6f  5272  dffun6  5273  dffun4f  5275  nffun  5282  funimaexglem  5342  nffv  5571  nffvmpt1  5572  dffn5imf  5619  funfvdm2f  5629  fvmptss2  5639  fvmpts  5642  fvmpt2  5648  fvmptssdm  5649  mptfvex  5650  fvmptdv  5653  fvmptd3  5658  elfvmptrab1  5659  eqfnfv2f  5666  ralrnmpt  5707  rexrnmpt  5708  f1ompt  5716  ffnfvf  5724  fmptco  5731  fmptcof  5732  fmptcos  5733  funiunfvdmf  5814  dff13f  5820  f1mpt  5821  fliftfuns  5848  nfiso  5856  nfriotadxy  5889  csbriotag  5893  riota2  5903  mpoeq123  5985  cbvmpox  6004  cbvmpo  6005  cbvmpov  6006  ovmpos  6050  ov2gf  6051  ovmpodxf  6052  ovmpodx  6053  ovmpodv  6059  ovmpodv2  6060  fvmpopr2d  6063  ovi3  6064  elovmporab  6127  elovmporab1w  6128  nfof  6145  nfofr  6146  offval2  6155  ofrfval2  6156  abrexex2g  6186  abrexex2  6190  uchoice  6204  dfopab2  6256  dfoprab3s  6257  mpomptsx  6264  dmmpossx  6266  fmpox  6267  mpofvex  6272  fnmpoovd  6282  fmpoco  6283  dfmpo  6290  f1od2  6302  disjxp1  6303  mpoxopoveq  6307  mpoxopovel  6308  nftpos  6346  tposoprab  6347  nfrecs  6374  nffrec  6463  eqerlem  6632  qliftfuns  6687  cbvixpv  6784  nfixpxy  6785  nfixp1  6786  ixpf  6788  mptelixpg  6802  dom2lem  6840  xpcomco  6894  xpf1o  6914  mapxpen  6918  ac6sfi  6968  opabfi  7008  nfsup  7067  nfdju  7117  exmidomni  7217  ismkvnex  7230  cc2  7350  cc4f  7352  cc4  7353  caucvgprprlemaddq  7792  caucvgsrlemgt1  7879  axpre-suploclemres  7985  lble  8991  supinfneg  9686  infsupneg  9687  fzrevral  10197  zsupcllemstep  10336  infssuzex  10340  infssuzcldc  10342  nfseq  10566  seq3f1olemstep  10623  seq3f1olemp  10624  nfwrd  10980  fimaxre2  11409  nfsum1  11538  nfsum  11539  cbvsumv  11543  cbvsumi  11544  sumfct  11556  sumrbdclem  11559  summodclem2a  11563  zsumdc  11566  fsum3  11569  isumss  11573  isumss2  11575  fsum3cvg2  11576  fsumzcl2  11587  fsumadd  11588  fsumsplitf  11590  sumsnf  11591  sumsn  11593  sumsns  11597  fsumsplitsnun  11601  fsum2dlemstep  11616  fisumcom2  11620  fsumshftm  11627  fsum00  11644  fsumrelem  11653  fsumiun  11659  mertenslem2  11718  prodeq1  11735  nfcprod1  11736  nfcprod  11737  cbvprod  11740  cbvprodv  11741  cbvprodi  11742  prodrbdclem  11753  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  fprodntrivap  11766  prodfct  11769  prodssdc  11771  prodsnf  11774  prodsn  11775  fprodm1s  11783  fprodp1s  11784  prodsns  11785  fprodcllemf  11795  fprodconst  11802  fprodap0  11803  fprod2dlemstep  11804  fprodcom2fi  11808  fprodrec  11811  fproddivapf  11813  fprodsplitf  11814  fprodap0f  11818  fprodle  11822  bezoutlemmain  12190  bezout  12203  nnwofdc  12230  nnwosdc  12231  prmind2  12313  oddpwdclemdvds  12363  oddpwdclemndvds  12364  pcmpt  12537  pcmptdvds  12539  ctiunctlemudc  12679  ctiunctlemf  12680  ctiunctlemfo  12681  ctiunct  12682  ctiunctal  12683  prdsbas3  12989  gsumfzconstf  13548  cnmpt11  14603  cnmpt1t  14605  cnmpt21  14611  cnmpt2t  14613  cnmptcom  14618  imasnopn  14619  fsumcncntop  14887  ellimc3apf  14980  ellimc3ap  14981  limcmpted  14983  dvmptfsum  15045  elplyd  15061  fsumdvdsmul  15311  lgseisenlem2  15396  elabf1  15511  elabf2  15512  elabg2  15515  bj-omssind  15665  bj-bdfindisg  15678  bj-nntrans  15681  bj-nnelirr  15683  bj-omtrans  15686  setindis  15697  bdsetindis  15699  bj-nn0sucALT  15708  bj-findis  15709  bj-findisg  15710  strcollnfALT  15716  isomninnlem  15761  trilpolemeq1  15771  trirec0  15775  iswomninnlem  15780  ismkvnnlem  15783  nconstwlpolemgt0  15795