Theorem nfcv 2348

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

Syntax hints:   e. wcel 2176   F/_wnfc 2335

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 1472  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-nfc 2337

This theorem is referenced by:  nfcvd  2349  nfel  2357  nfeq1  2358  nfel1  2359  nfeq2  2360  nfel2  2361  nfcvf  2371  r2al  2525  r2ex  2526  nfraldxy  2539  nfrexdxy  2540  nfra2xy  2548  r19.12  2612  ralcom  2669  rexcom  2670  nfreudxy  2680  raleq  2702  rexeq  2703  reueq1  2704  rmoeq1  2705  cbvralw  2732  cbvrexw  2733  cbvral  2734  cbvrex  2735  rabeq  2764  rabeqi  2765  cbvrabv  2771  vtoclg  2833  vtocl2g  2837  vtoclga  2839  vtocl2ga  2841  vtocl3ga  2843  spcimdv  2857  spcimedv  2859  spcgv  2860  spcegv  2861  rspct  2870  rspc  2871  rspce  2872  rspc2  2888  ceqsexg  2901  elabgt  2914  elabf  2916  elabg  2919  elab3g  2924  elrab  2929  mob  2955  nfsbc1v  3017  elrabsf  3037  sbcralt  3075  sbcrext  3076  sbcralg  3077  sbcrex  3078  sbcreug  3079  cbvcsbv  3099  csbconstg  3107  nfcsb1v  3126  csbie  3139  csbnestg  3148  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  cbvralv2  3160  cbvrexv2  3161  dfss4st  3406  n0rf  3473  n0r  3474  eq0  3479  raaanlem  3565  nfpw  3629  cbviunv  3966  cbviinv  3967  ssiun2s  3971  iunab  3974  ssiinf  3977  ssiin  3978  iinab  3989  cbvdisjv  4032  nfdisjv  4033  disjnims  4036  disji2  4037  cbvmptv  4140  triun  4155  csbexga  4172  repizf2  4206  moop2  4296  euotd  4299  opelopabgf  4316  opelopabf  4321  nfpo  4348  nfso  4349  pofun  4359  nfse  4388  nffrfor  4395  nffr  4396  frind  4399  nfwe  4402  eusvnf  4500  rabxfrd  4516  tfis  4631  tfisi  4635  opeliunxp  4730  nfrel  4760  opeliunxp2  4818  ralxpf  4824  rexxpf  4825  nfco  4843  nfcnv  4857  dfdmf  4871  dfrnf  4919  nfdm  4922  nfres  4961  resmptf  5009  nfiotadw  5235  dffun6f  5284  dffun6  5285  dffun4f  5287  nffun  5294  funimaexglem  5357  nffv  5586  nffvmpt1  5587  dffn5imf  5634  funfvdm2f  5644  fvmptss2  5654  fvmpts  5657  fvmpt2  5663  fvmptssdm  5664  mptfvex  5665  fvmptdv  5668  fvmptd3  5673  elfvmptrab1  5674  eqfnfv2f  5681  ralrnmpt  5722  rexrnmpt  5723  f1ompt  5731  ffnfvf  5739  fmptco  5746  fmptcof  5747  fmptcos  5748  funiunfvdmf  5833  dff13f  5839  f1mpt  5840  fliftfuns  5867  nfiso  5875  nfriotadxy  5908  csbriotag  5912  riota2  5922  mpoeq123  6004  cbvmpox  6023  cbvmpo  6024  cbvmpov  6025  ovmpos  6069  ov2gf  6070  ovmpodxf  6071  ovmpodx  6072  ovmpodv  6078  ovmpodv2  6079  fvmpopr2d  6082  ovi3  6083  elovmporab  6146  elovmporab1w  6147  nfof  6164  nfofr  6165  offval2  6174  ofrfval2  6175  abrexex2g  6205  abrexex2  6209  uchoice  6223  dfopab2  6275  dfoprab3s  6276  mpomptsx  6283  dmmpossx  6285  fmpox  6286  mpofvex  6291  fnmpoovd  6301  fmpoco  6302  dfmpo  6309  f1od2  6321  disjxp1  6322  mpoxopoveq  6326  mpoxopovel  6327  nftpos  6365  tposoprab  6366  nfrecs  6393  nffrec  6482  eqerlem  6651  qliftfuns  6706  cbvixpv  6803  nfixpxy  6804  nfixp1  6805  ixpf  6807  mptelixpg  6821  dom2lem  6863  xpcomco  6921  xpf1o  6941  mapxpen  6945  ac6sfi  6995  opabfi  7035  nfsup  7094  nfdju  7144  exmidomni  7244  ismkvnex  7257  cc2  7379  cc4f  7381  cc4  7382  caucvgprprlemaddq  7821  caucvgsrlemgt1  7908  axpre-suploclemres  8014  lble  9020  supinfneg  9716  infsupneg  9717  fzrevral  10227  zsupcllemstep  10372  infssuzex  10376  infssuzcldc  10378  nfseq  10602  seq3f1olemstep  10659  seq3f1olemp  10660  nfwrd  11022  fimaxre2  11538  nfsum1  11667  nfsum  11668  cbvsumv  11672  cbvsumi  11673  sumfct  11685  sumrbdclem  11688  summodclem2a  11692  zsumdc  11695  fsum3  11698  isumss  11702  isumss2  11704  fsum3cvg2  11705  fsumzcl2  11716  fsumadd  11717  fsumsplitf  11719  sumsnf  11720  sumsn  11722  sumsns  11726  fsumsplitsnun  11730  fsum2dlemstep  11745  fisumcom2  11749  fsumshftm  11756  fsum00  11773  fsumrelem  11782  fsumiun  11788  mertenslem2  11847  prodeq1  11864  nfcprod1  11865  nfcprod  11866  cbvprod  11869  cbvprodv  11870  cbvprodi  11871  prodrbdclem  11882  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  fprodntrivap  11895  prodfct  11898  prodssdc  11900  prodsnf  11903  prodsn  11904  fprodm1s  11912  fprodp1s  11913  prodsns  11914  fprodcllemf  11924  fprodconst  11931  fprodap0  11932  fprod2dlemstep  11933  fprodcom2fi  11937  fprodrec  11940  fproddivapf  11942  fprodsplitf  11943  fprodap0f  11947  fprodle  11951  bezoutlemmain  12319  bezout  12332  nnwofdc  12359  nnwosdc  12360  prmind2  12442  oddpwdclemdvds  12492  oddpwdclemndvds  12493  pcmpt  12666  pcmptdvds  12668  ctiunctlemudc  12808  ctiunctlemf  12809  ctiunctlemfo  12810  ctiunct  12811  ctiunctal  12812  prdsbas3  13119  gsumfzconstf  13678  cnmpt11  14755  cnmpt1t  14757  cnmpt21  14763  cnmpt2t  14765  cnmptcom  14770  imasnopn  14771  fsumcncntop  15039  ellimc3apf  15132  ellimc3ap  15133  limcmpted  15135  dvmptfsum  15197  elplyd  15213  fsumdvdsmul  15463  lgseisenlem2  15548  gropd  15644  grstructd2dom  15645  elabf1  15717  elabf2  15718  elabg2  15721  bj-omssind  15871  bj-bdfindisg  15884  bj-nntrans  15887  bj-nnelirr  15889  bj-omtrans  15892  setindis  15903  bdsetindis  15905  bj-nn0sucALT  15914  bj-findis  15915  bj-findisg  15916  strcollnfALT  15922  isomninnlem  15969  trilpolemeq1  15979  trirec0  15983  iswomninnlem  15988  ismkvnnlem  15991  nconstwlpolemgt0  16003