Theorem nfcv 2372

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

Syntax hints:   e. wcel 2200   F/_wnfc 2359

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 1495  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-nfc 2361

This theorem is referenced by:  nfcvd  2373  nfel  2381  nfeq1  2382  nfel1  2383  nfeq2  2384  nfel2  2385  nfcvf  2395  r2al  2549  r2ex  2550  nfraldxy  2563  nfrexdxy  2564  nfra2xy  2572  r19.12  2637  ralcom  2694  rexcom  2695  nfreudxy  2705  raleq  2728  rexeq  2729  reueq1  2730  rmoeq1  2731  cbvralw  2758  cbvrexw  2759  cbvral  2761  cbvrex  2762  rabeq  2791  rabeqi  2792  cbvrabv  2798  vtoclg  2861  vtocl2g  2865  vtoclga  2867  vtocl2ga  2869  vtocl3ga  2871  spcimdv  2887  spcimedv  2889  spcgv  2890  spcegv  2891  rspct  2900  rspc  2901  rspce  2902  rspc2  2918  ceqsexg  2931  elabgt  2944  elabf  2946  elabg  2949  elab3g  2954  elrab  2959  mob  2985  nfsbc1v  3047  elrabsf  3067  sbcralt  3105  sbcrext  3106  sbcralg  3107  sbcrex  3108  sbcreug  3109  reu8nf  3110  cbvcsbv  3130  csbconstg  3138  nfcsb1v  3157  csbie  3170  csbnestg  3179  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  cbvralv2  3191  cbvrexv2  3192  dfss4st  3437  n0rf  3504  n0r  3505  eq0  3510  raaanlem  3596  nfpw  3662  cbviunv  4004  cbviinv  4005  ssiun2s  4009  iunab  4012  ssiinf  4015  ssiin  4016  iinab  4027  cbvdisjv  4070  nfdisjv  4071  disjnims  4074  disji2  4075  invdisjrab  4077  cbvmptv  4180  triun  4195  csbexga  4212  repizf2  4246  moop2  4338  euotd  4341  opelopabgf  4358  opelopabf  4363  nfpo  4392  nfso  4393  pofun  4403  nfse  4432  nffrfor  4439  nffr  4440  frind  4443  nfwe  4446  eusvnf  4544  rabxfrd  4560  tfis  4675  tfisi  4679  opeliunxp  4774  nfrel  4804  opeliunxp2  4862  ralxpf  4868  rexxpf  4869  nfco  4887  nfcnv  4901  dfdmf  4916  dfrnf  4965  nfdm  4968  nfres  5007  resmptf  5055  nfiotadw  5281  dffun6f  5331  dffun6  5332  dffun4f  5334  nffun  5341  funimaexglem  5404  nffv  5639  nffvmpt1  5640  dffn5imf  5691  funfvdm2f  5701  fvmptss2  5711  fvmpts  5714  fvmpt2  5720  fvmptssdm  5721  mptfvex  5722  fvmptdv  5725  fvmptd3  5730  elfvmptrab1  5731  eqfnfv2f  5738  ralrnmpt  5779  rexrnmpt  5780  f1ompt  5788  ffnfvf  5796  fmptco  5803  fmptcof  5804  fmptcos  5805  funiunfvdmf  5894  dff13f  5900  f1mpt  5901  fliftfuns  5928  nfiso  5936  nfriotadxy  5969  csbriotag  5974  riota2  5984  mpoeq123  6069  cbvmpox  6088  cbvmpo  6089  cbvmpov  6090  ovmpos  6134  ov2gf  6135  ovmpodxf  6136  ovmpodx  6137  ovmpodv  6143  ovmpodv2  6144  fvmpopr2d  6147  ovi3  6148  elovmporab  6211  elovmporab1w  6212  nfof  6230  nfofr  6231  offval2  6240  ofrfval2  6241  abrexex2g  6271  abrexex2  6275  uchoice  6289  dfopab2  6341  dfoprab3s  6342  mpomptsx  6349  dmmpossx  6351  fmpox  6352  mpofvex  6357  fnmpoovd  6367  fmpoco  6368  dfmpo  6375  f1od2  6387  disjxp1  6388  mpoxopoveq  6392  mpoxopovel  6393  nftpos  6431  tposoprab  6432  nfrecs  6459  nffrec  6548  eqerlem  6719  qliftfuns  6774  cbvixpv  6871  nfixpxy  6872  nfixp1  6873  ixpf  6875  mptelixpg  6889  dom2lem  6931  xpcomco  6993  xpf1o  7013  mapxpen  7017  ac6sfi  7068  opabfi  7108  nfsup  7167  nfdju  7217  exmidomni  7317  ismkvnex  7330  cc2  7461  cc4f  7463  cc4  7464  caucvgprprlemaddq  7903  caucvgsrlemgt1  7990  axpre-suploclemres  8096  lble  9102  supinfneg  9798  infsupneg  9799  fzrevral  10309  zsupcllemstep  10457  infssuzex  10461  infssuzcldc  10463  nfseq  10687  seq3f1olemstep  10744  seq3f1olemp  10745  nfwrd  11108  reuccatpfxs1v  11288  fimaxre2  11746  nfsum1  11875  nfsum  11876  cbvsumv  11880  cbvsumi  11881  sumfct  11893  sumrbdclem  11896  summodclem2a  11900  zsumdc  11903  fsum3  11906  isumss  11910  isumss2  11912  fsum3cvg2  11913  fsumzcl2  11924  fsumadd  11925  fsumsplitf  11927  sumsnf  11928  sumsn  11930  sumsns  11934  fsumsplitsnun  11938  fsum2dlemstep  11953  fisumcom2  11957  fsumshftm  11964  fsum00  11981  fsumrelem  11990  fsumiun  11996  mertenslem2  12055  prodeq1  12072  nfcprod1  12073  nfcprod  12074  cbvprod  12077  cbvprodv  12078  cbvprodi  12079  prodrbdclem  12090  prodmodclem2a  12095  zproddc  12098  fprodseq  12102  fprodntrivap  12103  prodfct  12106  prodssdc  12108  prodsnf  12111  prodsn  12112  fprodm1s  12120  fprodp1s  12121  prodsns  12122  fprodcllemf  12132  fprodconst  12139  fprodap0  12140  fprod2dlemstep  12141  fprodcom2fi  12145  fprodrec  12148  fproddivapf  12150  fprodsplitf  12151  fprodap0f  12155  fprodle  12159  bezoutlemmain  12527  bezout  12540  nnwofdc  12567  nnwosdc  12568  prmind2  12650  oddpwdclemdvds  12700  oddpwdclemndvds  12701  pcmpt  12874  pcmptdvds  12876  ctiunctlemudc  13016  ctiunctlemf  13017  ctiunctlemfo  13018  ctiunct  13019  ctiunctal  13020  prdsbas3  13328  gsumfzconstf  13887  cnmpt11  14965  cnmpt1t  14967  cnmpt21  14973  cnmpt2t  14975  cnmptcom  14980  imasnopn  14981  fsumcncntop  15249  ellimc3apf  15342  ellimc3ap  15343  limcmpted  15345  dvmptfsum  15407  elplyd  15423  fsumdvdsmul  15673  lgseisenlem2  15758  gropd  15856  grstructd2dom  15857  lfgrnloopen  15939  elabf1  16169  elabf2  16170  elabg2  16173  bj-omssind  16322  bj-bdfindisg  16335  bj-nntrans  16338  bj-nnelirr  16340  bj-omtrans  16343  setindis  16354  bdsetindis  16356  bj-nn0sucALT  16365  bj-findis  16366  bj-findisg  16367  strcollnfALT  16373  isomninnlem  16425  trilpolemeq1  16435  trirec0  16439  iswomninnlem  16444  ismkvnnlem  16447  nconstwlpolemgt0  16459