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  invdisjrab  4039  cbvmptv  4141  triun  4156  csbexga  4173  repizf2  4207  moop2  4297  euotd  4300  opelopabgf  4317  opelopabf  4322  nfpo  4349  nfso  4350  pofun  4360  nfse  4389  nffrfor  4396  nffr  4397  frind  4400  nfwe  4403  eusvnf  4501  rabxfrd  4517  tfis  4632  tfisi  4636  opeliunxp  4731  nfrel  4761  opeliunxp2  4819  ralxpf  4825  rexxpf  4826  nfco  4844  nfcnv  4858  dfdmf  4872  dfrnf  4920  nfdm  4923  nfres  4962  resmptf  5010  nfiotadw  5236  dffun6f  5285  dffun6  5286  dffun4f  5288  nffun  5295  funimaexglem  5358  nffv  5588  nffvmpt1  5589  dffn5imf  5636  funfvdm2f  5646  fvmptss2  5656  fvmpts  5659  fvmpt2  5665  fvmptssdm  5666  mptfvex  5667  fvmptdv  5670  fvmptd3  5675  elfvmptrab1  5676  eqfnfv2f  5683  ralrnmpt  5724  rexrnmpt  5725  f1ompt  5733  ffnfvf  5741  fmptco  5748  fmptcof  5749  fmptcos  5750  funiunfvdmf  5835  dff13f  5841  f1mpt  5842  fliftfuns  5869  nfiso  5877  nfriotadxy  5910  csbriotag  5914  riota2  5924  mpoeq123  6006  cbvmpox  6025  cbvmpo  6026  cbvmpov  6027  ovmpos  6071  ov2gf  6072  ovmpodxf  6073  ovmpodx  6074  ovmpodv  6080  ovmpodv2  6081  fvmpopr2d  6084  ovi3  6085  elovmporab  6148  elovmporab1w  6149  nfof  6166  nfofr  6167  offval2  6176  ofrfval2  6177  abrexex2g  6207  abrexex2  6211  uchoice  6225  dfopab2  6277  dfoprab3s  6278  mpomptsx  6285  dmmpossx  6287  fmpox  6288  mpofvex  6293  fnmpoovd  6303  fmpoco  6304  dfmpo  6311  f1od2  6323  disjxp1  6324  mpoxopoveq  6328  mpoxopovel  6329  nftpos  6367  tposoprab  6368  nfrecs  6395  nffrec  6484  eqerlem  6653  qliftfuns  6708  cbvixpv  6805  nfixpxy  6806  nfixp1  6807  ixpf  6809  mptelixpg  6823  dom2lem  6865  xpcomco  6923  xpf1o  6943  mapxpen  6947  ac6sfi  6997  opabfi  7037  nfsup  7096  nfdju  7146  exmidomni  7246  ismkvnex  7259  cc2  7381  cc4f  7383  cc4  7384  caucvgprprlemaddq  7823  caucvgsrlemgt1  7910  axpre-suploclemres  8016  lble  9022  supinfneg  9718  infsupneg  9719  fzrevral  10229  zsupcllemstep  10374  infssuzex  10378  infssuzcldc  10380  nfseq  10604  seq3f1olemstep  10661  seq3f1olemp  10662  nfwrd  11024  fimaxre2  11571  nfsum1  11700  nfsum  11701  cbvsumv  11705  cbvsumi  11706  sumfct  11718  sumrbdclem  11721  summodclem2a  11725  zsumdc  11728  fsum3  11731  isumss  11735  isumss2  11737  fsum3cvg2  11738  fsumzcl2  11749  fsumadd  11750  fsumsplitf  11752  sumsnf  11753  sumsn  11755  sumsns  11759  fsumsplitsnun  11763  fsum2dlemstep  11778  fisumcom2  11782  fsumshftm  11789  fsum00  11806  fsumrelem  11815  fsumiun  11821  mertenslem2  11880  prodeq1  11897  nfcprod1  11898  nfcprod  11899  cbvprod  11902  cbvprodv  11903  cbvprodi  11904  prodrbdclem  11915  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  fprodntrivap  11928  prodfct  11931  prodssdc  11933  prodsnf  11936  prodsn  11937  fprodm1s  11945  fprodp1s  11946  prodsns  11947  fprodcllemf  11957  fprodconst  11964  fprodap0  11965  fprod2dlemstep  11966  fprodcom2fi  11970  fprodrec  11973  fproddivapf  11975  fprodsplitf  11976  fprodap0f  11980  fprodle  11984  bezoutlemmain  12352  bezout  12365  nnwofdc  12392  nnwosdc  12393  prmind2  12475  oddpwdclemdvds  12525  oddpwdclemndvds  12526  pcmpt  12699  pcmptdvds  12701  ctiunctlemudc  12841  ctiunctlemf  12842  ctiunctlemfo  12843  ctiunct  12844  ctiunctal  12845  prdsbas3  13152  gsumfzconstf  13711  cnmpt11  14788  cnmpt1t  14790  cnmpt21  14796  cnmpt2t  14798  cnmptcom  14803  imasnopn  14804  fsumcncntop  15072  ellimc3apf  15165  ellimc3ap  15166  limcmpted  15168  dvmptfsum  15230  elplyd  15246  fsumdvdsmul  15496  lgseisenlem2  15581  gropd  15677  grstructd2dom  15678  elabf1  15754  elabf2  15755  elabg2  15758  bj-omssind  15908  bj-bdfindisg  15921  bj-nntrans  15924  bj-nnelirr  15926  bj-omtrans  15929  setindis  15940  bdsetindis  15942  bj-nn0sucALT  15951  bj-findis  15952  bj-findisg  15953  strcollnfALT  15959  isomninnlem  16006  trilpolemeq1  16016  trirec0  16020  iswomninnlem  16025  ismkvnnlem  16028  nconstwlpolemgt0  16040