Theorem nfcv 2392

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

Syntax hints:   e. wcel 2209   F/_wnfc 2379

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 1502  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-nfc 2381

This theorem is referenced by:  nfcvd  2393  nfel  2401  nfeq1  2402  nfel1  2403  nfeq2  2404  nfel2  2405  nfcvf  2415  r2al  2569  r2ex  2570  nfraldxy  2583  nfrexdxy  2584  nfra2xy  2592  r19.12  2657  ralcom  2714  rexcom  2715  nfreudxy  2725  raleq  2749  rexeq  2750  reueq1  2751  rmoeq1  2752  cbvralw  2779  cbvrexw  2780  cbvral  2782  cbvrex  2783  rabeq  2813  rabeqi  2814  cbvrabv  2820  vtoclg  2883  vtocl2g  2887  vtoclga  2889  vtocl2ga  2891  vtocl3ga  2893  spcimdv  2909  spcimedv  2911  spcgv  2912  spcegv  2913  rspct  2922  rspc  2923  rspce  2924  rspc2  2941  ceqsexg  2954  elabgt  2967  elabf  2969  elabg  2972  elab3g  2977  elrab  2982  mob  3008  nfsbc1v  3070  elrabsf  3090  sbcralt  3128  sbcrext  3129  sbcralg  3130  sbcrex  3131  sbcreug  3132  reu8nf  3133  cbvcsbv  3153  csbconstg  3161  nfcsb1v  3180  csbie  3193  csbnestg  3202  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  cbvralv2  3214  cbvrexv2  3215  dfss4st  3464  n0rf  3534  n0r  3535  eq0  3540  raaanlem  3629  nfpw  3701  cbviunv  4046  cbviinv  4047  ssiun2s  4051  iunab  4054  ssiinf  4057  ssiin  4058  iinab  4069  cbvdisjv  4112  nfdisjv  4113  disjnims  4116  disji2  4117  invdisjrab  4119  cbvmptv  4222  triun  4237  csbexga  4256  repizf2  4294  moop2  4387  euotd  4390  opelopabgf  4407  opelopabf  4412  nfpo  4441  nfso  4442  pofun  4452  nfse  4481  nffrfor  4488  nffr  4489  frind  4492  nfwe  4495  eusvnf  4594  rabxfrd  4610  tfis  4725  tfisi  4729  opeliunxp  4825  nfrel  4855  opeliunxp2  4915  ralxpf  4921  rexxpf  4922  nfco  4940  nfcnv  4954  dfdmf  4969  dfrnf  5018  nfdm  5021  nfres  5060  resmptf  5108  nfiotadw  5335  dffun6f  5385  dffun6  5386  dffun4f  5388  nffun  5395  funimaexglem  5459  nffv  5700  nffvmpt1  5701  dffn5imf  5752  funfvdm2f  5762  fvmptss2  5774  fvmpts  5777  fvmpt2  5783  fvmptssdm  5784  mptfvex  5785  fvmptdv  5788  fvmptd3  5793  elfvmptrab1  5794  eqfnfv2f  5801  ralrnmpt  5841  rexrnmpt  5842  f1ompt  5850  ffnfvf  5858  fmptco  5865  fmptcof  5866  fmptcos  5867  dfimafnf  5945  funiunfvdmf  5960  dff13f  5966  f1mpt  5967  fliftfuns  5994  nfiso  6002  nfriotadxy  6037  csbriotag  6042  riota2  6052  mpoeq123  6137  cbvmpox  6156  cbvmpo  6157  cbvmpov  6158  ovmpos  6202  ov2gf  6203  ovmpodxf  6204  ovmpodx  6205  ovmpodv  6211  ovmpodv2  6212  fvmpopr2d  6215  ovi3  6216  elovmporab  6279  elovmporab1w  6280  nfof  6298  nfofr  6299  offval2  6308  ofrfval2  6309  abrexex2g  6339  abrexex2  6343  uchoice  6361  dfopab2  6413  dfoprab3s  6414  mpomptsx  6423  dmmpossx  6425  fmpox  6426  mpofvex  6431  fnmpoovd  6441  fmpoco  6442  dfmpo  6449  f1od2  6461  disjxp1  6462  mpoxopoveq  6501  mpoxopovel  6502  nftpos  6540  tposoprab  6541  nfrecs  6568  nffrec  6657  eqerlem  6828  qliftfuns  6883  cbvixpv  6988  nfixpxy  6989  nfixp1  6990  ixpf  6992  mptelixpg  7006  dom2lem  7048  modom  7098  xpcomco  7114  xpf1o  7134  mapxpen  7138  ac6sfi  7192  opabfi  7237  nfsup  7322  nfdju  7372  exmidomni  7472  ismkvnex  7485  cc2  7623  cc4f  7625  cc4  7626  caucvgprprlemaddq  8065  caucvgsrlemgt1  8152  axpre-suploclemres  8258  lble  9267  supinfneg  9974  infsupneg  9975  fzrevral  10490  zsupcllemstep  10640  infssuzex  10644  infssuzcldc  10646  infssfzcldc  10647  infssfzledc  10648  nfseq  10872  seq3f1olemstep  10929  seq3f1olemp  10930  nfwrd  11311  reuccatpfxs1v  11498  fimaxre2  11971  nfsum1  12100  nfsum  12101  cbvsumv  12105  cbvsumi  12106  sumfct  12118  sumrbdclem  12122  summodclem2a  12126  zsumdc  12129  fsum3  12132  isumss  12136  isumss2  12138  fsum3cvg2  12139  fsumzcl2  12150  fsumadd  12151  fsumsplitf  12153  sumsnf  12154  sumsn  12156  sumsns  12160  fsumsplitsnun  12164  fsum2dlemstep  12179  fisumcom2  12183  fsumshftm  12190  fsum00  12207  fsumrelem  12216  fsumiun  12222  mertenslem2  12281  prodeq1  12298  nfcprod1  12299  nfcprod  12300  cbvprod  12303  cbvprodv  12304  cbvprodi  12305  prodrbdclem  12316  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  fprodntrivap  12329  prodfct  12332  prodssdc  12334  prodsnf  12337  prodsn  12338  fprodm1s  12346  fprodp1s  12347  prodsns  12348  fprodcllemf  12358  fprodconst  12365  fprodap0  12366  fprod2dlemstep  12367  fprodcom2fi  12371  fprodrec  12374  fproddivapf  12376  fprodsplitf  12377  fprodap0f  12381  fprodle  12385  bezoutlemmain  12753  bezout  12766  nnwofdc  12793  nnwosdc  12794  prmind2  12876  oddpwdclemdvds  12926  oddpwdclemndvds  12927  pcmpt  13100  pcmptdvds  13102  ctiunctlemudc  13306  ctiunctlemf  13307  ctiunctlemfo  13308  ctiunct  13309  ctiunctal  13310  gzsumconstf  14121  gzsumsplit0  14125  gsumsncmn  14133  gsummptfidmadd  14138  prdsbas3  14164  cnmpt11  15307  cnmpt1t  15309  cnmpt21  15315  cnmpt2t  15317  cnmptcom  15322  imasnopn  15323  fsumcncntop  15591  ellimc3apf  15684  ellimc3ap  15685  limcmpted  15687  dvmptfsum  15749  elplyd  15765  fsumdvdsmul  16019  lgseisenlem2  16104  gropd  16202  grstructd2dom  16203  lfgrnloopen  16288  elabf1  16723  elabf2  16724  elabg2  16727  bj-omssind  16875  bj-bdfindisg  16888  bj-nntrans  16891  bj-nnelirr  16893  bj-omtrans  16896  setindis  16907  bdsetindis  16909  bj-nn0sucALT  16918  bj-findis  16919  bj-findisg  16920  strcollnfALT  16926  isomninnlem  16984  trilpolemeq1  16994  trirec0  16998  iswomninnlem  17004  ismkvnnlem  17007  nconstwlpolemgt0  17019