Theorem nfcv 2336

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

Syntax hints:   e. wcel 2164   F/_wnfc 2323

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 1460  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-nfc 2325

This theorem is referenced by:  nfcvd  2337  nfel  2345  nfeq1  2346  nfel1  2347  nfeq2  2348  nfel2  2349  nfcvf  2359  r2al  2513  r2ex  2514  nfraldxy  2527  nfrexdxy  2528  nfra2xy  2536  r19.12  2600  ralcom  2657  rexcom  2658  nfreudxy  2668  raleq  2690  rexeq  2691  reueq1  2692  rmoeq1  2693  cbvralw  2720  cbvrexw  2721  cbvral  2722  cbvrex  2723  rabeq  2752  rabeqi  2753  cbvrabv  2759  vtoclg  2820  vtocl2g  2824  vtoclga  2826  vtocl2ga  2828  vtocl3ga  2830  spcimdv  2844  spcimedv  2846  spcgv  2847  spcegv  2848  rspct  2857  rspc  2858  rspce  2859  rspc2  2875  ceqsexg  2888  elabgt  2901  elabf  2903  elabg  2906  elab3g  2911  elrab  2916  mob  2942  nfsbc1v  3004  elrabsf  3024  sbcralt  3062  sbcrext  3063  sbcralg  3064  sbcrex  3065  sbcreug  3066  cbvcsbv  3086  csbconstg  3094  nfcsb1v  3113  csbie  3126  csbnestg  3135  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  cbvralv2  3147  cbvrexv2  3148  dfss4st  3392  n0rf  3459  n0r  3460  eq0  3465  raaanlem  3551  nfpw  3614  cbviunv  3951  cbviinv  3952  ssiun2s  3956  iunab  3959  ssiinf  3962  ssiin  3963  iinab  3974  cbvdisjv  4017  nfdisjv  4018  disjnims  4021  disji2  4022  cbvmptv  4125  triun  4140  csbexga  4157  repizf2  4191  moop2  4280  euotd  4283  opelopabgf  4300  opelopabf  4305  nfpo  4332  nfso  4333  pofun  4343  nfse  4372  nffrfor  4379  nffr  4380  frind  4383  nfwe  4386  eusvnf  4484  rabxfrd  4500  tfis  4615  tfisi  4619  opeliunxp  4714  nfrel  4744  opeliunxp2  4802  ralxpf  4808  rexxpf  4809  nfco  4827  nfcnv  4841  dfdmf  4855  dfrnf  4903  nfdm  4906  nfres  4944  resmptf  4992  nfiotadw  5218  dffun6f  5267  dffun6  5268  dffun4f  5270  nffun  5277  funimaexglem  5337  nffv  5564  nffvmpt1  5565  dffn5imf  5612  funfvdm2f  5622  fvmptss2  5632  fvmpts  5635  fvmpt2  5641  fvmptssdm  5642  mptfvex  5643  fvmptdv  5646  fvmptd3  5651  elfvmptrab1  5652  eqfnfv2f  5659  ralrnmpt  5700  rexrnmpt  5701  f1ompt  5709  ffnfvf  5717  fmptco  5724  fmptcof  5725  fmptcos  5726  funiunfvdmf  5807  dff13f  5813  f1mpt  5814  fliftfuns  5841  nfiso  5849  nfriotadxy  5882  csbriotag  5886  riota2  5896  mpoeq123  5977  cbvmpox  5996  cbvmpo  5997  cbvmpov  5998  ovmpos  6042  ov2gf  6043  ovmpodxf  6044  ovmpodx  6045  ovmpodv  6051  ovmpodv2  6052  ovi3  6055  elovmporab  6118  elovmporab1w  6119  nfof  6136  nfofr  6137  offval2  6146  ofrfval2  6147  abrexex2g  6172  abrexex2  6176  uchoice  6190  dfopab2  6242  dfoprab3s  6243  mpomptsx  6250  dmmpossx  6252  fmpox  6253  mpofvex  6256  fnmpoovd  6268  fmpoco  6269  dfmpo  6276  f1od2  6288  disjxp1  6289  mpoxopoveq  6293  mpoxopovel  6294  nftpos  6332  tposoprab  6333  nfrecs  6360  nffrec  6449  eqerlem  6618  qliftfuns  6673  cbvixpv  6770  nfixpxy  6771  nfixp1  6772  ixpf  6774  mptelixpg  6788  dom2lem  6826  xpcomco  6880  xpf1o  6900  mapxpen  6904  ac6sfi  6954  opabfi  6992  nfsup  7051  nfdju  7101  exmidomni  7201  ismkvnex  7214  cc2  7327  cc4f  7329  cc4  7330  caucvgprprlemaddq  7768  caucvgsrlemgt1  7855  axpre-suploclemres  7961  lble  8966  supinfneg  9660  infsupneg  9661  fzrevral  10171  nfseq  10528  seq3f1olemstep  10585  seq3f1olemp  10586  nfwrd  10942  fimaxre2  11370  nfsum1  11499  nfsum  11500  cbvsumv  11504  cbvsumi  11505  sumfct  11517  sumrbdclem  11520  summodclem2a  11524  zsumdc  11527  fsum3  11530  isumss  11534  isumss2  11536  fsum3cvg2  11537  fsumzcl2  11548  fsumadd  11549  fsumsplitf  11551  sumsnf  11552  sumsn  11554  sumsns  11558  fsumsplitsnun  11562  fsum2dlemstep  11577  fisumcom2  11581  fsumshftm  11588  fsum00  11605  fsumrelem  11614  fsumiun  11620  mertenslem2  11679  prodeq1  11696  nfcprod1  11697  nfcprod  11698  cbvprod  11701  cbvprodv  11702  cbvprodi  11703  prodrbdclem  11714  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  fprodntrivap  11727  prodfct  11730  prodssdc  11732  prodsnf  11735  prodsn  11736  fprodm1s  11744  fprodp1s  11745  prodsns  11746  fprodcllemf  11756  fprodconst  11763  fprodap0  11764  fprod2dlemstep  11765  fprodcom2fi  11769  fprodrec  11772  fproddivapf  11774  fprodsplitf  11775  fprodap0f  11779  fprodle  11783  zsupcllemstep  12082  infssuzex  12086  infssuzcldc  12088  bezoutlemmain  12135  bezout  12148  nnwofdc  12175  nnwosdc  12176  prmind2  12258  oddpwdclemdvds  12308  oddpwdclemndvds  12309  pcmpt  12481  pcmptdvds  12483  ctiunctlemudc  12594  ctiunctlemf  12595  ctiunctlemfo  12596  ctiunct  12597  ctiunctal  12598  gsumfzconstf  13412  cnmpt11  14451  cnmpt1t  14453  cnmpt21  14459  cnmpt2t  14461  cnmptcom  14466  imasnopn  14467  fsumcncntop  14724  ellimc3apf  14814  ellimc3ap  14815  limcmpted  14817  elplyd  14887  lgseisenlem2  15187  elabf1  15273  elabf2  15274  elabg2  15277  bj-omssind  15427  bj-bdfindisg  15440  bj-nntrans  15443  bj-nnelirr  15445  bj-omtrans  15448  setindis  15459  bdsetindis  15461  bj-nn0sucALT  15470  bj-findis  15471  bj-findisg  15472  strcollnfALT  15478  isomninnlem  15520  trilpolemeq1  15530  trirec0  15534  iswomninnlem  15539  ismkvnnlem  15542  nconstwlpolemgt0  15554