Theorem nfcv 2375

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

Syntax hints:   e. wcel 2202   F/_wnfc 2362

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 1498  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-nfc 2364

This theorem is referenced by:  nfcvd  2376  nfel  2384  nfeq1  2385  nfel1  2386  nfeq2  2387  nfel2  2388  nfcvf  2398  r2al  2552  r2ex  2553  nfraldxy  2566  nfrexdxy  2567  nfra2xy  2575  r19.12  2640  ralcom  2697  rexcom  2698  nfreudxy  2708  raleq  2731  rexeq  2732  reueq1  2733  rmoeq1  2734  cbvralw  2761  cbvrexw  2762  cbvral  2764  cbvrex  2765  rabeq  2795  rabeqi  2796  cbvrabv  2802  vtoclg  2865  vtocl2g  2869  vtoclga  2871  vtocl2ga  2873  vtocl3ga  2875  spcimdv  2891  spcimedv  2893  spcgv  2894  spcegv  2895  rspct  2904  rspc  2905  rspce  2906  rspc2  2922  ceqsexg  2935  elabgt  2948  elabf  2950  elabg  2953  elab3g  2958  elrab  2963  mob  2989  nfsbc1v  3051  elrabsf  3071  sbcralt  3109  sbcrext  3110  sbcralg  3111  sbcrex  3112  sbcreug  3113  reu8nf  3114  cbvcsbv  3134  csbconstg  3142  nfcsb1v  3161  csbie  3174  csbnestg  3183  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  cbvralv2  3195  cbvrexv2  3196  dfss4st  3442  n0rf  3509  n0r  3510  eq0  3515  raaanlem  3601  nfpw  3669  cbviunv  4014  cbviinv  4015  ssiun2s  4019  iunab  4022  ssiinf  4025  ssiin  4026  iinab  4037  cbvdisjv  4080  nfdisjv  4081  disjnims  4084  disji2  4085  invdisjrab  4087  cbvmptv  4190  triun  4205  csbexga  4222  repizf2  4258  moop2  4350  euotd  4353  opelopabgf  4370  opelopabf  4375  nfpo  4404  nfso  4405  pofun  4415  nfse  4444  nffrfor  4451  nffr  4452  frind  4455  nfwe  4458  eusvnf  4556  rabxfrd  4572  tfis  4687  tfisi  4691  opeliunxp  4787  nfrel  4817  opeliunxp2  4876  ralxpf  4882  rexxpf  4883  nfco  4901  nfcnv  4915  dfdmf  4930  dfrnf  4979  nfdm  4982  nfres  5021  resmptf  5069  nfiotadw  5296  dffun6f  5346  dffun6  5347  dffun4f  5349  nffun  5356  funimaexglem  5420  nffv  5658  nffvmpt1  5659  dffn5imf  5710  funfvdm2f  5720  fvmptss2  5730  fvmpts  5733  fvmpt2  5739  fvmptssdm  5740  mptfvex  5741  fvmptdv  5744  fvmptd3  5749  elfvmptrab1  5750  eqfnfv2f  5757  ralrnmpt  5797  rexrnmpt  5798  f1ompt  5806  ffnfvf  5814  fmptco  5821  fmptcof  5822  fmptcos  5823  funiunfvdmf  5915  dff13f  5921  f1mpt  5922  fliftfuns  5949  nfiso  5957  nfriotadxy  5990  csbriotag  5995  riota2  6005  mpoeq123  6090  cbvmpox  6109  cbvmpo  6110  cbvmpov  6111  ovmpos  6155  ov2gf  6156  ovmpodxf  6157  ovmpodx  6158  ovmpodv  6164  ovmpodv2  6165  fvmpopr2d  6168  ovi3  6169  elovmporab  6232  elovmporab1w  6233  nfof  6250  nfofr  6251  offval2  6260  ofrfval2  6261  abrexex2g  6291  abrexex2  6295  uchoice  6309  dfopab2  6361  dfoprab3s  6362  mpomptsx  6371  dmmpossx  6373  fmpox  6374  mpofvex  6379  fnmpoovd  6389  fmpoco  6390  dfmpo  6397  f1od2  6409  disjxp1  6410  mpoxopoveq  6449  mpoxopovel  6450  nftpos  6488  tposoprab  6489  nfrecs  6516  nffrec  6605  eqerlem  6776  qliftfuns  6831  cbvixpv  6928  nfixpxy  6929  nfixp1  6930  ixpf  6932  mptelixpg  6946  dom2lem  6988  modom  7037  xpcomco  7053  xpf1o  7073  mapxpen  7077  ac6sfi  7130  opabfi  7175  nfsup  7251  nfdju  7301  exmidomni  7401  ismkvnex  7414  cc2  7546  cc4f  7548  cc4  7549  caucvgprprlemaddq  7988  caucvgsrlemgt1  8075  axpre-suploclemres  8181  lble  9186  supinfneg  9890  infsupneg  9891  fzrevral  10402  zsupcllemstep  10552  infssuzex  10556  infssuzcldc  10558  nfseq  10782  seq3f1olemstep  10839  seq3f1olemp  10840  nfwrd  11208  reuccatpfxs1v  11395  fimaxre2  11867  nfsum1  11996  nfsum  11997  cbvsumv  12001  cbvsumi  12002  sumfct  12014  sumrbdclem  12018  summodclem2a  12022  zsumdc  12025  fsum3  12028  isumss  12032  isumss2  12034  fsum3cvg2  12035  fsumzcl2  12046  fsumadd  12047  fsumsplitf  12049  sumsnf  12050  sumsn  12052  sumsns  12056  fsumsplitsnun  12060  fsum2dlemstep  12075  fisumcom2  12079  fsumshftm  12086  fsum00  12103  fsumrelem  12112  fsumiun  12118  mertenslem2  12177  prodeq1  12194  nfcprod1  12195  nfcprod  12196  cbvprod  12199  cbvprodv  12200  cbvprodi  12201  prodrbdclem  12212  prodmodclem2a  12217  zproddc  12220  fprodseq  12224  fprodntrivap  12225  prodfct  12228  prodssdc  12230  prodsnf  12233  prodsn  12234  fprodm1s  12242  fprodp1s  12243  prodsns  12244  fprodcllemf  12254  fprodconst  12261  fprodap0  12262  fprod2dlemstep  12263  fprodcom2fi  12267  fprodrec  12270  fproddivapf  12272  fprodsplitf  12273  fprodap0f  12277  fprodle  12281  bezoutlemmain  12649  bezout  12662  nnwofdc  12689  nnwosdc  12690  prmind2  12772  oddpwdclemdvds  12822  oddpwdclemndvds  12823  pcmpt  12996  pcmptdvds  12998  ctiunctlemudc  13138  ctiunctlemf  13139  ctiunctlemfo  13140  ctiunct  13141  ctiunctal  13142  prdsbas3  13450  gsumfzconstf  14009  gsumsplit0  14013  cnmpt11  15094  cnmpt1t  15096  cnmpt21  15102  cnmpt2t  15104  cnmptcom  15109  imasnopn  15110  fsumcncntop  15378  ellimc3apf  15471  ellimc3ap  15472  limcmpted  15474  dvmptfsum  15536  elplyd  15552  fsumdvdsmul  15805  lgseisenlem2  15890  gropd  15988  grstructd2dom  15989  lfgrnloopen  16074  elabf1  16499  elabf2  16500  elabg2  16503  bj-omssind  16651  bj-bdfindisg  16664  bj-nntrans  16667  bj-nnelirr  16669  bj-omtrans  16672  setindis  16683  bdsetindis  16685  bj-nn0sucALT  16694  bj-findis  16695  bj-findisg  16696  strcollnfALT  16702  isomninnlem  16762  trilpolemeq1  16772  trirec0  16776  iswomninnlem  16782  ismkvnnlem  16785  nconstwlpolemgt0  16797  gfsumsn  16814