Theorem nfcv 2319

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

Syntax hints:   e. wcel 2148   F/_wnfc 2306

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 1449  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-nfc 2308

This theorem is referenced by:  nfcvd  2320  nfel  2328  nfeq1  2329  nfel1  2330  nfeq2  2331  nfel2  2332  nfcvf  2342  r2al  2496  r2ex  2497  nfraldxy  2510  nfrexdxy  2511  nfra2xy  2519  r19.12  2583  ralcom  2640  rexcom  2641  nfreudxy  2650  raleq  2672  rexeq  2673  reueq1  2674  rmoeq1  2675  cbvralw  2698  cbvral  2699  cbvrex  2700  rabeq  2729  rabeqi  2730  cbvrabv  2736  vtoclg  2797  vtocl2g  2801  vtoclga  2803  vtocl2ga  2805  vtocl3ga  2807  spcimdv  2821  spcimedv  2823  spcgv  2824  spcegv  2825  rspct  2834  rspc  2835  rspce  2836  rspc2  2852  ceqsexg  2865  elabgt  2878  elabf  2880  elabg  2883  elab3g  2888  elrab  2893  mob  2919  nfsbc1v  2981  elrabsf  3001  sbcralt  3039  sbcrext  3040  sbcralg  3041  sbcrex  3042  sbcreug  3043  cbvcsbv  3063  csbconstg  3071  nfcsb1v  3090  csbie  3102  csbnestg  3111  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  cbvralv2  3123  cbvrexv2  3124  dfss4st  3368  n0rf  3435  n0r  3436  eq0  3441  raaanlem  3528  nfpw  3588  cbviunv  3925  cbviinv  3926  ssiun2s  3930  iunab  3933  ssiinf  3936  ssiin  3937  iinab  3948  cbvdisjv  3991  nfdisjv  3992  disjnims  3995  disji2  3996  cbvmptv  4099  triun  4114  csbexga  4131  repizf2  4162  moop2  4251  euotd  4254  opelopabf  4274  nfpo  4301  nfso  4302  pofun  4312  nfse  4341  nffrfor  4348  nffr  4349  frind  4352  nfwe  4355  eusvnf  4453  rabxfrd  4469  tfis  4582  tfisi  4586  opeliunxp  4681  nfrel  4711  opeliunxp2  4767  ralxpf  4773  rexxpf  4774  nfco  4792  nfcnv  4806  dfdmf  4820  dfrnf  4868  nfdm  4871  nfres  4909  resmptf  4957  nfiotadw  5181  dffun6f  5229  dffun6  5230  dffun4f  5232  nffun  5239  funimaexglem  5299  nffv  5525  nffvmpt1  5526  dffn5imf  5571  funfvdm2f  5581  fvmptss2  5591  fvmpts  5594  fvmpt2  5599  fvmptssdm  5600  mptfvex  5601  fvmptdv  5604  fvmptd3  5609  elfvmptrab1  5610  eqfnfv2f  5617  ralrnmpt  5658  rexrnmpt  5659  f1ompt  5667  ffnfvf  5675  fmptco  5682  fmptcof  5683  fmptcos  5684  funiunfvdmf  5764  dff13f  5770  f1mpt  5771  fliftfuns  5798  nfiso  5806  nfriotadxy  5838  csbriotag  5842  riota2  5852  mpoeq123  5933  cbvmpox  5952  cbvmpo  5953  cbvmpov  5954  ovmpos  5997  ov2gf  5998  ovmpodxf  5999  ovmpodx  6000  ovmpodv  6006  ovmpodv2  6007  ovi3  6010  nfof  6087  nfofr  6088  offval2  6097  ofrfval2  6098  abrexex2g  6120  abrexex2  6124  dfopab2  6189  dfoprab3s  6190  mpomptsx  6197  dmmpossx  6199  fmpox  6200  mpofvex  6203  fnmpoovd  6215  fmpoco  6216  dfmpo  6223  f1od2  6235  disjxp1  6236  mpoxopoveq  6240  mpoxopovel  6241  nftpos  6279  tposoprab  6280  nfrecs  6307  nffrec  6396  eqerlem  6565  qliftfuns  6618  cbvixpv  6715  nfixpxy  6716  nfixp1  6717  ixpf  6719  mptelixpg  6733  dom2lem  6771  xpcomco  6825  xpf1o  6843  mapxpen  6847  ac6sfi  6897  nfsup  6990  nfdju  7040  exmidomni  7139  ismkvnex  7152  cc2  7265  cc4f  7267  cc4  7268  caucvgprprlemaddq  7706  caucvgsrlemgt1  7793  axpre-suploclemres  7899  lble  8902  supinfneg  9593  infsupneg  9594  fzrevral  10102  nfseq  10452  seq3f1olemstep  10498  seq3f1olemp  10499  fimaxre2  11230  nfsum1  11359  nfsum  11360  cbvsumv  11364  cbvsumi  11365  sumfct  11377  sumrbdclem  11380  summodclem2a  11384  zsumdc  11387  fsum3  11390  isumss  11394  isumss2  11396  fsum3cvg2  11397  fsumzcl2  11408  fsumadd  11409  fsumsplitf  11411  sumsnf  11412  sumsn  11414  sumsns  11418  fsumsplitsnun  11422  fsum2dlemstep  11437  fisumcom2  11441  fsumshftm  11448  fsum00  11465  fsumrelem  11474  fsumiun  11480  mertenslem2  11539  prodeq1  11556  nfcprod1  11557  nfcprod  11558  cbvprod  11561  cbvprodv  11562  cbvprodi  11563  prodrbdclem  11574  prodmodclem2a  11579  zproddc  11582  fprodseq  11586  fprodntrivap  11587  prodfct  11590  prodssdc  11592  prodsnf  11595  prodsn  11596  fprodm1s  11604  fprodp1s  11605  prodsns  11606  fprodcllemf  11616  fprodconst  11623  fprodap0  11624  fprod2dlemstep  11625  fprodcom2fi  11629  fprodrec  11632  fproddivapf  11634  fprodsplitf  11635  fprodap0f  11639  fprodle  11643  zsupcllemstep  11940  infssuzex  11944  infssuzcldc  11946  bezoutlemmain  11993  bezout  12006  nnwofdc  12033  nnwosdc  12034  prmind2  12114  oddpwdclemdvds  12164  oddpwdclemndvds  12165  pcmpt  12335  pcmptdvds  12337  ctiunctlemudc  12432  ctiunctlemf  12433  ctiunctlemfo  12434  ctiunct  12435  ctiunctal  12436  cnmpt11  13676  cnmpt1t  13678  cnmpt21  13684  cnmpt2t  13686  cnmptcom  13691  imasnopn  13692  fsumcncntop  13949  ellimc3apf  14022  ellimc3ap  14023  limcmpted  14025  elabf1  14415  elabf2  14416  elabg2  14419  bj-omssind  14569  bj-bdfindisg  14582  bj-nntrans  14585  bj-nnelirr  14587  bj-omtrans  14590  setindis  14601  bdsetindis  14603  bj-nn0sucALT  14612  bj-findis  14613  bj-findisg  14614  strcollnfALT  14620  isomninnlem  14660  trilpolemeq1  14670  trirec0  14674  iswomninnlem  14679  ismkvnnlem  14682  nconstwlpolemgt0  14693