Theorem nfcv 2308

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

Syntax hints:   e. wcel 2136   F/_wnfc 2295

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 1437  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-nfc 2297

This theorem is referenced by:  nfcvd  2309  nfel  2317  nfeq1  2318  nfel1  2319  nfeq2  2320  nfel2  2321  nfcvf  2331  r2al  2485  r2ex  2486  nfraldxy  2499  nfrexdxy  2500  nfra2xy  2508  r19.12  2572  ralcom  2629  rexcom  2630  nfreudxy  2639  raleq  2661  rexeq  2662  reueq1  2663  rmoeq1  2664  cbvralw  2687  cbvral  2688  cbvrex  2689  rabeq  2718  rabeqi  2719  cbvrabv  2725  vtoclg  2786  vtocl2g  2790  vtoclga  2792  vtocl2ga  2794  vtocl3ga  2796  spcimdv  2810  spcimedv  2812  spcgv  2813  spcegv  2814  rspct  2823  rspc  2824  rspce  2825  rspc2  2841  ceqsexg  2854  elabgt  2867  elabf  2869  elabg  2872  elab3g  2877  elrab  2882  mob  2908  nfsbc1v  2969  elrabsf  2989  sbcralt  3027  sbcrext  3028  sbcralg  3029  sbcrex  3030  sbcreug  3031  cbvcsbv  3051  csbconstg  3059  nfcsb1v  3078  csbie  3090  csbnestg  3099  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  cbvralv2  3111  cbvrexv2  3112  dfss4st  3355  n0rf  3421  n0r  3422  eq0  3427  raaanlem  3514  nfpw  3572  cbviunv  3905  cbviinv  3906  ssiun2s  3910  iunab  3912  ssiinf  3915  ssiin  3916  iinab  3927  cbvdisjv  3970  nfdisjv  3971  disjnims  3974  disji2  3975  cbvmptv  4078  triun  4093  csbexga  4110  repizf2  4141  moop2  4229  euotd  4232  opelopabf  4252  nfpo  4279  nfso  4280  pofun  4290  nfse  4319  nffrfor  4326  nffr  4327  frind  4330  nfwe  4333  eusvnf  4431  rabxfrd  4447  tfis  4560  tfisi  4564  opeliunxp  4659  nfrel  4689  opeliunxp2  4744  ralxpf  4750  rexxpf  4751  nfco  4769  nfcnv  4783  dfdmf  4797  dfrnf  4845  nfdm  4848  nfres  4886  resmptf  4934  nfiotadw  5156  dffun6f  5201  dffun6  5202  dffun4f  5204  nffun  5211  funimaexglem  5271  nffv  5496  nffvmpt1  5497  dffn5imf  5541  funfvdm2f  5551  fvmptss2  5561  fvmpts  5564  fvmpt2  5569  fvmptssdm  5570  mptfvex  5571  fvmptdv  5574  fvmptd3  5579  elfvmptrab1  5580  eqfnfv2f  5587  ralrnmpt  5627  rexrnmpt  5628  f1ompt  5636  ffnfvf  5644  fmptco  5651  fmptcof  5652  fmptcos  5653  funiunfvdmf  5732  dff13f  5738  f1mpt  5739  fliftfuns  5766  nfiso  5774  nfriotadxy  5806  csbriotag  5810  riota2  5820  mpoeq123  5901  cbvmpox  5920  cbvmpo  5921  cbvmpov  5922  ovmpos  5965  ov2gf  5966  ovmpodxf  5967  ovmpodx  5968  ovmpodv  5974  ovmpodv2  5975  ovi3  5978  nfof  6055  nfofr  6056  offval2  6065  ofrfval2  6066  abrexex2g  6088  abrexex2  6092  dfopab2  6157  dfoprab3s  6158  mpomptsx  6165  dmmpossx  6167  fmpox  6168  mpofvex  6171  fnmpoovd  6183  fmpoco  6184  dfmpo  6191  f1od2  6203  disjxp1  6204  mpoxopoveq  6208  mpoxopovel  6209  nftpos  6247  tposoprab  6248  nfrecs  6275  nffrec  6364  eqerlem  6532  qliftfuns  6585  cbvixpv  6682  nfixpxy  6683  nfixp1  6684  ixpf  6686  mptelixpg  6700  dom2lem  6738  xpcomco  6792  xpf1o  6810  mapxpen  6814  ac6sfi  6864  nfsup  6957  nfdju  7007  exmidomni  7106  ismkvnex  7119  cc2  7208  cc4f  7210  cc4  7211  caucvgprprlemaddq  7649  caucvgsrlemgt1  7736  axpre-suploclemres  7842  lble  8842  supinfneg  9533  infsupneg  9534  fzrevral  10040  nfseq  10390  seq3f1olemstep  10436  seq3f1olemp  10437  fimaxre2  11168  nfsum1  11297  nfsum  11298  cbvsumv  11302  cbvsumi  11303  sumfct  11315  sumrbdclem  11318  summodclem2a  11322  zsumdc  11325  fsum3  11328  isumss  11332  isumss2  11334  fsum3cvg2  11335  fsumzcl2  11346  fsumadd  11347  fsumsplitf  11349  sumsnf  11350  sumsn  11352  sumsns  11356  fsumsplitsnun  11360  fsum2dlemstep  11375  fisumcom2  11379  fsumshftm  11386  fsum00  11403  fsumrelem  11412  fsumiun  11418  mertenslem2  11477  prodeq1  11494  nfcprod1  11495  nfcprod  11496  cbvprod  11499  cbvprodv  11500  cbvprodi  11501  prodrbdclem  11512  prodmodclem2a  11517  zproddc  11520  fprodseq  11524  fprodntrivap  11525  prodfct  11528  prodssdc  11530  prodsnf  11533  prodsn  11534  fprodm1s  11542  fprodp1s  11543  prodsns  11544  fprodcllemf  11554  fprodconst  11561  fprodap0  11562  fprod2dlemstep  11563  fprodcom2fi  11567  fprodrec  11570  fproddivapf  11572  fprodsplitf  11573  fprodap0f  11577  fprodle  11581  zsupcllemstep  11878  infssuzex  11882  infssuzcldc  11884  bezoutlemmain  11931  bezout  11944  nnwofdc  11971  nnwosdc  11972  prmind2  12052  oddpwdclemdvds  12102  oddpwdclemndvds  12103  pcmpt  12273  pcmptdvds  12275  ctiunctlemudc  12370  ctiunctlemf  12371  ctiunctlemfo  12372  ctiunct  12373  ctiunctal  12374  cnmpt11  12923  cnmpt1t  12925  cnmpt21  12931  cnmpt2t  12933  cnmptcom  12938  imasnopn  12939  fsumcncntop  13196  ellimc3apf  13269  ellimc3ap  13270  limcmpted  13272  elabf1  13662  elabf2  13663  elabg2  13666  bj-omssind  13817  bj-bdfindisg  13830  bj-nntrans  13833  bj-nnelirr  13835  bj-omtrans  13838  setindis  13849  bdsetindis  13851  bj-nn0sucALT  13860  bj-findis  13861  bj-findisg  13862  strcollnfALT  13868  isomninnlem  13909  trilpolemeq1  13919  trirec0  13923  iswomninnlem  13928  ismkvnnlem  13931  nconstwlpolemgt0  13942