Theorem nfcv 2312

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

Syntax hints:   e. wcel 2141   F/_wnfc 2299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-nfc 2301

This theorem is referenced by:  nfcvd  2313  nfel  2321  nfeq1  2322  nfel1  2323  nfeq2  2324  nfel2  2325  nfcvf  2335  r2al  2489  r2ex  2490  nfraldxy  2503  nfrexdxy  2504  nfra2xy  2512  r19.12  2576  ralcom  2633  rexcom  2634  nfreudxy  2643  raleq  2665  rexeq  2666  reueq1  2667  rmoeq1  2668  cbvralw  2691  cbvral  2692  cbvrex  2693  rabeq  2722  rabeqi  2723  cbvrabv  2729  vtoclg  2790  vtocl2g  2794  vtoclga  2796  vtocl2ga  2798  vtocl3ga  2800  spcimdv  2814  spcimedv  2816  spcgv  2817  spcegv  2818  rspct  2827  rspc  2828  rspce  2829  rspc2  2845  ceqsexg  2858  elabgt  2871  elabf  2873  elabg  2876  elab3g  2881  elrab  2886  mob  2912  nfsbc1v  2973  elrabsf  2993  sbcralt  3031  sbcrext  3032  sbcralg  3033  sbcrex  3034  sbcreug  3035  cbvcsbv  3055  csbconstg  3063  nfcsb1v  3082  csbie  3094  csbnestg  3103  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  cbvralv2  3115  cbvrexv2  3116  dfss4st  3360  n0rf  3427  n0r  3428  eq0  3433  raaanlem  3520  nfpw  3579  cbviunv  3912  cbviinv  3913  ssiun2s  3917  iunab  3919  ssiinf  3922  ssiin  3923  iinab  3934  cbvdisjv  3977  nfdisjv  3978  disjnims  3981  disji2  3982  cbvmptv  4085  triun  4100  csbexga  4117  repizf2  4148  moop2  4236  euotd  4239  opelopabf  4259  nfpo  4286  nfso  4287  pofun  4297  nfse  4326  nffrfor  4333  nffr  4334  frind  4337  nfwe  4340  eusvnf  4438  rabxfrd  4454  tfis  4567  tfisi  4571  opeliunxp  4666  nfrel  4696  opeliunxp2  4751  ralxpf  4757  rexxpf  4758  nfco  4776  nfcnv  4790  dfdmf  4804  dfrnf  4852  nfdm  4855  nfres  4893  resmptf  4941  nfiotadw  5163  dffun6f  5211  dffun6  5212  dffun4f  5214  nffun  5221  funimaexglem  5281  nffv  5506  nffvmpt1  5507  dffn5imf  5551  funfvdm2f  5561  fvmptss2  5571  fvmpts  5574  fvmpt2  5579  fvmptssdm  5580  mptfvex  5581  fvmptdv  5584  fvmptd3  5589  elfvmptrab1  5590  eqfnfv2f  5597  ralrnmpt  5638  rexrnmpt  5639  f1ompt  5647  ffnfvf  5655  fmptco  5662  fmptcof  5663  fmptcos  5664  funiunfvdmf  5743  dff13f  5749  f1mpt  5750  fliftfuns  5777  nfiso  5785  nfriotadxy  5817  csbriotag  5821  riota2  5831  mpoeq123  5912  cbvmpox  5931  cbvmpo  5932  cbvmpov  5933  ovmpos  5976  ov2gf  5977  ovmpodxf  5978  ovmpodx  5979  ovmpodv  5985  ovmpodv2  5986  ovi3  5989  nfof  6066  nfofr  6067  offval2  6076  ofrfval2  6077  abrexex2g  6099  abrexex2  6103  dfopab2  6168  dfoprab3s  6169  mpomptsx  6176  dmmpossx  6178  fmpox  6179  mpofvex  6182  fnmpoovd  6194  fmpoco  6195  dfmpo  6202  f1od2  6214  disjxp1  6215  mpoxopoveq  6219  mpoxopovel  6220  nftpos  6258  tposoprab  6259  nfrecs  6286  nffrec  6375  eqerlem  6544  qliftfuns  6597  cbvixpv  6694  nfixpxy  6695  nfixp1  6696  ixpf  6698  mptelixpg  6712  dom2lem  6750  xpcomco  6804  xpf1o  6822  mapxpen  6826  ac6sfi  6876  nfsup  6969  nfdju  7019  exmidomni  7118  ismkvnex  7131  cc2  7229  cc4f  7231  cc4  7232  caucvgprprlemaddq  7670  caucvgsrlemgt1  7757  axpre-suploclemres  7863  lble  8863  supinfneg  9554  infsupneg  9555  fzrevral  10061  nfseq  10411  seq3f1olemstep  10457  seq3f1olemp  10458  fimaxre2  11190  nfsum1  11319  nfsum  11320  cbvsumv  11324  cbvsumi  11325  sumfct  11337  sumrbdclem  11340  summodclem2a  11344  zsumdc  11347  fsum3  11350  isumss  11354  isumss2  11356  fsum3cvg2  11357  fsumzcl2  11368  fsumadd  11369  fsumsplitf  11371  sumsnf  11372  sumsn  11374  sumsns  11378  fsumsplitsnun  11382  fsum2dlemstep  11397  fisumcom2  11401  fsumshftm  11408  fsum00  11425  fsumrelem  11434  fsumiun  11440  mertenslem2  11499  prodeq1  11516  nfcprod1  11517  nfcprod  11518  cbvprod  11521  cbvprodv  11522  cbvprodi  11523  prodrbdclem  11534  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodntrivap  11547  prodfct  11550  prodssdc  11552  prodsnf  11555  prodsn  11556  fprodm1s  11564  fprodp1s  11565  prodsns  11566  fprodcllemf  11576  fprodconst  11583  fprodap0  11584  fprod2dlemstep  11585  fprodcom2fi  11589  fprodrec  11592  fproddivapf  11594  fprodsplitf  11595  fprodap0f  11599  fprodle  11603  zsupcllemstep  11900  infssuzex  11904  infssuzcldc  11906  bezoutlemmain  11953  bezout  11966  nnwofdc  11993  nnwosdc  11994  prmind2  12074  oddpwdclemdvds  12124  oddpwdclemndvds  12125  pcmpt  12295  pcmptdvds  12297  ctiunctlemudc  12392  ctiunctlemf  12393  ctiunctlemfo  12394  ctiunct  12395  ctiunctal  12396  cnmpt11  13077  cnmpt1t  13079  cnmpt21  13085  cnmpt2t  13087  cnmptcom  13092  imasnopn  13093  fsumcncntop  13350  ellimc3apf  13423  ellimc3ap  13424  limcmpted  13426  elabf1  13816  elabf2  13817  elabg2  13820  bj-omssind  13970  bj-bdfindisg  13983  bj-nntrans  13986  bj-nnelirr  13988  bj-omtrans  13991  setindis  14002  bdsetindis  14004  bj-nn0sucALT  14013  bj-findis  14014  bj-findisg  14015  strcollnfALT  14021  isomninnlem  14062  trilpolemeq1  14072  trirec0  14076  iswomninnlem  14081  ismkvnnlem  14084  nconstwlpolemgt0  14095