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  2651  raleq  2673  rexeq  2674  reueq1  2675  rmoeq1  2676  cbvralw  2699  cbvral  2700  cbvrex  2701  rabeq  2730  rabeqi  2731  cbvrabv  2737  vtoclg  2798  vtocl2g  2802  vtoclga  2804  vtocl2ga  2806  vtocl3ga  2808  spcimdv  2822  spcimedv  2824  spcgv  2825  spcegv  2826  rspct  2835  rspc  2836  rspce  2837  rspc2  2853  ceqsexg  2866  elabgt  2879  elabf  2881  elabg  2884  elab3g  2889  elrab  2894  mob  2920  nfsbc1v  2982  elrabsf  3002  sbcralt  3040  sbcrext  3041  sbcralg  3042  sbcrex  3043  sbcreug  3044  cbvcsbv  3064  csbconstg  3072  nfcsb1v  3091  csbie  3103  csbnestg  3112  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  cbvralv2  3124  cbvrexv2  3125  dfss4st  3369  n0rf  3436  n0r  3437  eq0  3442  raaanlem  3529  nfpw  3589  cbviunv  3926  cbviinv  3927  ssiun2s  3931  iunab  3934  ssiinf  3937  ssiin  3938  iinab  3949  cbvdisjv  3992  nfdisjv  3993  disjnims  3996  disji2  3997  cbvmptv  4100  triun  4115  csbexga  4132  repizf2  4163  moop2  4252  euotd  4255  opelopabf  4275  nfpo  4302  nfso  4303  pofun  4313  nfse  4342  nffrfor  4349  nffr  4350  frind  4353  nfwe  4356  eusvnf  4454  rabxfrd  4470  tfis  4583  tfisi  4587  opeliunxp  4682  nfrel  4712  opeliunxp2  4768  ralxpf  4774  rexxpf  4775  nfco  4793  nfcnv  4807  dfdmf  4821  dfrnf  4869  nfdm  4872  nfres  4910  resmptf  4958  nfiotadw  5182  dffun6f  5230  dffun6  5231  dffun4f  5233  nffun  5240  funimaexglem  5300  nffv  5526  nffvmpt1  5527  dffn5imf  5572  funfvdm2f  5582  fvmptss2  5592  fvmpts  5595  fvmpt2  5600  fvmptssdm  5601  mptfvex  5602  fvmptdv  5605  fvmptd3  5610  elfvmptrab1  5611  eqfnfv2f  5618  ralrnmpt  5659  rexrnmpt  5660  f1ompt  5668  ffnfvf  5676  fmptco  5683  fmptcof  5684  fmptcos  5685  funiunfvdmf  5765  dff13f  5771  f1mpt  5772  fliftfuns  5799  nfiso  5807  nfriotadxy  5839  csbriotag  5843  riota2  5853  mpoeq123  5934  cbvmpox  5953  cbvmpo  5954  cbvmpov  5955  ovmpos  5998  ov2gf  5999  ovmpodxf  6000  ovmpodx  6001  ovmpodv  6007  ovmpodv2  6008  ovi3  6011  nfof  6088  nfofr  6089  offval2  6098  ofrfval2  6099  abrexex2g  6121  abrexex2  6125  dfopab2  6190  dfoprab3s  6191  mpomptsx  6198  dmmpossx  6200  fmpox  6201  mpofvex  6204  fnmpoovd  6216  fmpoco  6217  dfmpo  6224  f1od2  6236  disjxp1  6237  mpoxopoveq  6241  mpoxopovel  6242  nftpos  6280  tposoprab  6281  nfrecs  6308  nffrec  6397  eqerlem  6566  qliftfuns  6619  cbvixpv  6716  nfixpxy  6717  nfixp1  6718  ixpf  6720  mptelixpg  6734  dom2lem  6772  xpcomco  6826  xpf1o  6844  mapxpen  6848  ac6sfi  6898  nfsup  6991  nfdju  7041  exmidomni  7140  ismkvnex  7153  cc2  7266  cc4f  7268  cc4  7269  caucvgprprlemaddq  7707  caucvgsrlemgt1  7794  axpre-suploclemres  7900  lble  8904  supinfneg  9595  infsupneg  9596  fzrevral  10105  nfseq  10455  seq3f1olemstep  10501  seq3f1olemp  10502  fimaxre2  11235  nfsum1  11364  nfsum  11365  cbvsumv  11369  cbvsumi  11370  sumfct  11382  sumrbdclem  11385  summodclem2a  11389  zsumdc  11392  fsum3  11395  isumss  11399  isumss2  11401  fsum3cvg2  11402  fsumzcl2  11413  fsumadd  11414  fsumsplitf  11416  sumsnf  11417  sumsn  11419  sumsns  11423  fsumsplitsnun  11427  fsum2dlemstep  11442  fisumcom2  11446  fsumshftm  11453  fsum00  11470  fsumrelem  11479  fsumiun  11485  mertenslem2  11544  prodeq1  11561  nfcprod1  11562  nfcprod  11563  cbvprod  11566  cbvprodv  11567  cbvprodi  11568  prodrbdclem  11579  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodntrivap  11592  prodfct  11595  prodssdc  11597  prodsnf  11600  prodsn  11601  fprodm1s  11609  fprodp1s  11610  prodsns  11611  fprodcllemf  11621  fprodconst  11628  fprodap0  11629  fprod2dlemstep  11630  fprodcom2fi  11634  fprodrec  11637  fproddivapf  11639  fprodsplitf  11640  fprodap0f  11644  fprodle  11648  zsupcllemstep  11946  infssuzex  11950  infssuzcldc  11952  bezoutlemmain  11999  bezout  12012  nnwofdc  12039  nnwosdc  12040  prmind2  12120  oddpwdclemdvds  12170  oddpwdclemndvds  12171  pcmpt  12341  pcmptdvds  12343  ctiunctlemudc  12438  ctiunctlemf  12439  ctiunctlemfo  12440  ctiunct  12441  ctiunctal  12442  cnmpt11  13786  cnmpt1t  13788  cnmpt21  13794  cnmpt2t  13796  cnmptcom  13801  imasnopn  13802  fsumcncntop  14059  ellimc3apf  14132  ellimc3ap  14133  limcmpted  14135  lgseisenlem2  14454  elabf1  14536  elabf2  14537  elabg2  14540  bj-omssind  14690  bj-bdfindisg  14703  bj-nntrans  14706  bj-nnelirr  14708  bj-omtrans  14711  setindis  14722  bdsetindis  14724  bj-nn0sucALT  14733  bj-findis  14734  bj-findisg  14735  strcollnfALT  14741  isomninnlem  14781  trilpolemeq1  14791  trirec0  14795  iswomninnlem  14800  ismkvnnlem  14803  nconstwlpolemgt0  14814