Theorem nfcv 2279

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

Syntax hints:   e. wcel 1480   F/_wnfc 2266

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

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-nfc 2268

This theorem is referenced by:  nfcvd  2280  nfel  2288  nfeq1  2289  nfel1  2290  nfeq2  2291  nfel2  2292  nfcvf  2301  r2al  2452  r2ex  2453  nfraldxy  2465  nfrexdxy  2466  nfra2xy  2473  r19.12  2536  ralcom  2592  rexcom  2593  nfreudxy  2602  raleq  2624  rexeq  2625  reueq1  2626  rmoeq1  2627  cbvral  2648  cbvrex  2649  rabeq  2673  rabeqi  2674  cbvrabv  2680  vtoclg  2741  vtocl2g  2745  vtoclga  2747  vtocl2ga  2749  vtocl3ga  2751  spcimdv  2765  spcimedv  2767  spcgv  2768  spcegv  2769  rspct  2777  rspc  2778  rspce  2779  rspc2  2795  ceqsexg  2808  elabgt  2820  elabf  2822  elabg  2825  elab3g  2830  elrab  2835  mob  2861  nfsbc1v  2922  elrabsf  2942  sbcralt  2980  sbcrext  2981  sbcralg  2982  sbcrex  2983  sbcreug  2984  cbvcsbv  3004  csbconstg  3011  nfcsb1v  3030  csbie  3040  csbnestg  3049  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  cbvralv2  3061  cbvrexv2  3062  dfss4st  3304  n0rf  3370  n0r  3371  eq0  3376  raaanlem  3463  nfpw  3518  cbviunv  3847  cbviinv  3848  ssiun2s  3852  iunab  3854  ssiinf  3857  ssiin  3858  iinab  3869  cbvdisjv  3912  nfdisjv  3913  disjnims  3916  disji2  3917  cbvmptv  4019  triun  4034  csbexga  4051  repizf2  4081  moop2  4168  euotd  4171  opelopabf  4191  nfpo  4218  nfso  4219  pofun  4229  nfse  4258  nffrfor  4265  nffr  4266  frind  4269  nfwe  4272  eusvnf  4369  rabxfrd  4385  tfis  4492  tfisi  4496  opeliunxp  4589  nfrel  4619  opeliunxp2  4674  ralxpf  4680  rexxpf  4681  nfco  4699  nfcnv  4713  dfdmf  4727  dfrnf  4775  nfdm  4778  nfres  4816  resmptf  4864  nfiotadw  5086  dffun6f  5131  dffun6  5132  dffun4f  5134  nffun  5141  funimaexglem  5201  nffv  5424  nffvmpt1  5425  dffn5imf  5469  funfvdm2f  5479  fvmptss2  5489  fvmpts  5492  fvmpt2  5497  fvmptssdm  5498  mptfvex  5499  fvmptdv  5502  fvmptd3  5507  elfvmptrab1  5508  eqfnfv2f  5515  ralrnmpt  5555  rexrnmpt  5556  f1ompt  5564  ffnfvf  5572  fmptco  5579  fmptcof  5580  fmptcos  5581  funiunfvdmf  5658  dff13f  5664  f1mpt  5665  fliftfuns  5692  nfiso  5700  nfriotadxy  5731  csbriotag  5735  riota2  5745  mpoeq123  5823  cbvmpox  5842  cbvmpo  5843  cbvmpov  5844  ovmpos  5887  ov2gf  5888  ovmpodxf  5889  ovmpodx  5890  ovmpodv  5896  ovmpodv2  5897  ovi3  5900  nfof  5980  nfofr  5981  offval2  5990  ofrfval2  5991  abrexex2g  6011  abrexex2  6015  dfopab2  6080  dfoprab3s  6081  mpomptsx  6088  dmmpossx  6090  fmpox  6091  mpofvex  6094  fnmpoovd  6105  fmpoco  6106  dfmpo  6113  f1od2  6125  disjxp1  6126  mpoxopoveq  6130  mpoxopovel  6131  nftpos  6169  tposoprab  6170  nfrecs  6197  nffrec  6286  eqerlem  6453  qliftfuns  6506  cbvixpv  6603  nfixpxy  6604  nfixp1  6605  ixpf  6607  mptelixpg  6621  dom2lem  6659  xpcomco  6713  xpf1o  6731  mapxpen  6735  ac6sfi  6785  nfsup  6872  nfdju  6920  exmidomni  7007  ismkvnex  7022  caucvgprprlemaddq  7509  caucvgsrlemgt1  7596  axpre-suploclemres  7702  lble  8698  supinfneg  9383  infsupneg  9384  fzrevral  9878  nfseq  10221  seq3f1olemstep  10267  seq3f1olemp  10268  fimaxre2  10991  nfsum1  11118  nfsum  11119  cbvsumv  11123  cbvsumi  11124  sumfct  11136  sumrbdclem  11138  summodclem2a  11143  zsumdc  11146  fsum3  11149  isumss  11153  isumss2  11155  fsum3cvg2  11156  fsumzcl2  11167  fsumadd  11168  fsumsplitf  11170  sumsnf  11171  sumsn  11173  sumsns  11177  fsumsplitsnun  11181  fsum2dlemstep  11196  fisumcom2  11200  fsumshftm  11207  fsum00  11224  fsumrelem  11233  fsumiun  11239  mertenslem2  11298  prodeq1  11315  nfcprod1  11316  nfcprod  11317  cbvprod  11320  cbvprodv  11321  cbvprodi  11322  prodrbdclem  11333  zsupcllemstep  11627  infssuzex  11631  infssuzcldc  11633  bezoutlemmain  11675  bezout  11688  prmind2  11790  oddpwdclemdvds  11837  oddpwdclemndvds  11838  ctiunctlemudc  11939  ctiunctlemf  11940  ctiunctlemfo  11941  ctiunct  11942  cnmpt11  12441  cnmpt1t  12443  cnmpt21  12449  cnmpt2t  12451  cnmptcom  12456  imasnopn  12457  fsumcncntop  12714  ellimc3apf  12787  ellimc3ap  12788  limcmpted  12790  elabf1  12977  elabf2  12978  elabg2  12981  bj-omssind  13122  bj-bdfindisg  13135  bj-nntrans  13138  bj-nnelirr  13140  bj-omtrans  13143  setindis  13154  bdsetindis  13156  bj-nn0sucALT  13165  bj-findis  13166  bj-findisg  13167  strcollnfALT  13173  isomninnlem  13214  trilpolemeq1  13222