Theorem nfcv 2240

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

Syntax hints:   e. wcel 1448   F/_wnfc 2227

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393  ax-17 1474

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-nfc 2229

This theorem is referenced by:  nfcvd  2241  nfel  2249  nfeq1  2250  nfel1  2251  nfeq2  2252  nfel2  2253  nfcvf  2262  r2al  2413  r2ex  2414  nfraldxy  2426  nfrexdxy  2427  nfra2xy  2434  r19.12  2497  ralcom  2552  rexcom  2553  nfreudxy  2562  raleq  2584  rexeq  2585  reueq1  2586  rmoeq1  2587  cbvral  2608  cbvrex  2609  rabeq  2633  rabeqi  2634  cbvrabv  2640  vtoclg  2701  vtocl2g  2705  vtoclga  2707  vtocl2ga  2709  vtocl3ga  2711  spcimdv  2725  spcimedv  2727  spcgv  2728  spcegv  2729  rspct  2737  rspc  2738  rspce  2739  rspc2  2754  ceqsexg  2767  elabgt  2779  elabf  2781  elabg  2783  elab3g  2788  elrab  2793  mob  2819  nfsbc1v  2880  elrabsf  2899  sbcralt  2937  sbcrext  2938  sbcralg  2939  sbcrex  2940  sbcreug  2941  cbvcsbv  2960  csbconstg  2967  nfcsb1v  2985  csbie  2995  csbnestg  3004  cbvralcsf  3012  cbvrexcsf  3013  cbvreucsf  3014  cbvrabcsf  3015  cbvralv2  3016  cbvrexv2  3017  dfss4st  3256  n0rf  3322  n0r  3323  eq0  3328  raaanlem  3415  nfpw  3470  cbviunv  3799  cbviinv  3800  ssiun2s  3804  iunab  3806  ssiinf  3809  ssiin  3810  iinab  3821  cbvdisjv  3863  nfdisjv  3864  disjnims  3867  disji2  3868  cbvmptv  3964  triun  3979  csbexga  3996  repizf2  4026  moop2  4111  euotd  4114  opelopabf  4134  nfpo  4161  nfso  4162  pofun  4172  nfse  4201  nffrfor  4208  nffr  4209  frind  4212  nfwe  4215  eusvnf  4312  rabxfrd  4328  tfis  4435  tfisi  4439  opeliunxp  4532  nfrel  4562  opeliunxp2  4617  ralxpf  4623  rexxpf  4624  nfco  4642  nfcnv  4656  dfdmf  4670  dfrnf  4718  nfdm  4721  nfres  4757  resmptf  4805  nfiotadxy  5027  dffun6f  5072  dffun6  5073  dffun4f  5075  nffun  5082  funimaexglem  5142  nffv  5363  nffvmpt1  5364  dffn5imf  5408  funfvdm2f  5418  fvmptss2  5428  fvmpts  5431  fvmpt2  5436  fvmptssdm  5437  mptfvex  5438  fvmptdv  5441  fvmptd3  5446  elfvmptrab1  5447  eqfnfv2f  5454  ralrnmpt  5494  rexrnmpt  5495  f1ompt  5503  ffnfvf  5511  fmptco  5518  fmptcof  5519  fmptcos  5520  funiunfvdmf  5597  dff13f  5603  f1mpt  5604  fliftfuns  5631  nfiso  5639  nfriotadxy  5670  csbriotag  5674  riota2  5684  mpoeq123  5762  cbvmpox  5781  cbvmpo  5782  cbvmpov  5783  ovmpos  5826  ov2gf  5827  ovmpodxf  5828  ovmpodx  5829  ovmpodv  5835  ovmpodv2  5836  ovi3  5839  nfof  5919  nfofr  5920  offval2  5928  ofrfval2  5929  abrexex2g  5949  abrexex2  5953  dfopab2  6017  dfoprab3s  6018  mpomptsx  6025  dmmpossx  6027  fmpox  6028  mpt2fvex  6031  fnmpoovd  6042  fmpoco  6043  dfmpo  6050  f1od2  6062  disjxp1  6063  mpoxopoveq  6067  mpoxopovel  6068  nftpos  6106  tposoprab  6107  nfrecs  6134  nffrec  6223  eqerlem  6390  qliftfuns  6443  cbvixpv  6540  nfixpxy  6541  nfixp1  6542  ixpf  6544  mptelixpg  6558  dom2lem  6596  xpcomco  6649  xpf1o  6667  mapxpen  6671  ac6sfi  6721  nfsup  6794  nfdju  6842  exmidomni  6926  caucvgprprlemaddq  7417  caucvgsrlemgt1  7490  lble  8563  supinfneg  9240  infsupneg  9241  fzrevral  9726  nfseq  10069  seq3f1olemstep  10115  seq3f1olemp  10116  fimaxre2  10837  nfsum1  10964  nfsum  10965  cbvsumv  10969  cbvsumi  10970  sumfct  10982  sumrbdclem  10984  summodclem2a  10989  zsumdc  10992  fsum3  10995  isumss  10999  isumss2  11001  fsum3cvg2  11002  fsumzcl2  11013  fsumadd  11014  fsumsplitf  11016  sumsnf  11017  sumsn  11019  sumsns  11023  fsumsplitsnun  11027  fsum2dlemstep  11042  fisumcom2  11046  fsumshftm  11053  fsum00  11070  fsumrelem  11079  fsumiun  11085  mertenslem2  11144  zsupcllemstep  11433  infssuzex  11437  infssuzcldc  11439  bezoutlemmain  11479  bezout  11492  prmind2  11594  oddpwdclemdvds  11640  oddpwdclemndvds  11641  cnmpt11  12233  cnmpt1t  12235  cnmpt21  12241  cnmpt2t  12243  cnmptcom  12248  imasnopn  12249  elabf1  12569  elabf2  12570  elabg2  12573  bj-omssind  12718  bj-bdfindisg  12731  bj-nntrans  12734  bj-nnelirr  12736  bj-omtrans  12739  setindis  12750  bdsetindis  12752  bj-nn0sucALT  12761  bj-findis  12762  bj-findisg  12763  strcollnfALT  12769  isomninnlem  12809  trilpolemeq1  12817