Theorem nfcv 2339

Description: If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfcv	⊢ Ⅎ𝑥𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem nfcv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1542	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
2	1	nfci 2329	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   ∈ wcel 2167  Ⅎwnfc 2326

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 1463  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-nfc 2328

This theorem is referenced by:  nfcvd  2340  nfel  2348  nfeq1  2349  nfel1  2350  nfeq2  2351  nfel2  2352  nfcvf  2362  r2al  2516  r2ex  2517  nfraldxy  2530  nfrexdxy  2531  nfra2xy  2539  r19.12  2603  ralcom  2660  rexcom  2661  nfreudxy  2671  raleq  2693  rexeq  2694  reueq1  2695  rmoeq1  2696  cbvralw  2723  cbvrexw  2724  cbvral  2725  cbvrex  2726  rabeq  2755  rabeqi  2756  cbvrabv  2762  vtoclg  2824  vtocl2g  2828  vtoclga  2830  vtocl2ga  2832  vtocl3ga  2834  spcimdv  2848  spcimedv  2850  spcgv  2851  spcegv  2852  rspct  2861  rspc  2862  rspce  2863  rspc2  2879  ceqsexg  2892  elabgt  2905  elabf  2907  elabg  2910  elab3g  2915  elrab  2920  mob  2946  nfsbc1v  3008  elrabsf  3028  sbcralt  3066  sbcrext  3067  sbcralg  3068  sbcrex  3069  sbcreug  3070  cbvcsbv  3090  csbconstg  3098  nfcsb1v  3117  csbie  3130  csbnestg  3139  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  cbvralv2  3151  cbvrexv2  3152  dfss4st  3397  n0rf  3464  n0r  3465  eq0  3470  raaanlem  3556  nfpw  3619  cbviunv  3956  cbviinv  3957  ssiun2s  3961  iunab  3964  ssiinf  3967  ssiin  3968  iinab  3979  cbvdisjv  4022  nfdisjv  4023  disjnims  4026  disji2  4027  cbvmptv  4130  triun  4145  csbexga  4162  repizf2  4196  moop2  4285  euotd  4288  opelopabgf  4305  opelopabf  4310  nfpo  4337  nfso  4338  pofun  4348  nfse  4377  nffrfor  4384  nffr  4385  frind  4388  nfwe  4391  eusvnf  4489  rabxfrd  4505  tfis  4620  tfisi  4624  opeliunxp  4719  nfrel  4749  opeliunxp2  4807  ralxpf  4813  rexxpf  4814  nfco  4832  nfcnv  4846  dfdmf  4860  dfrnf  4908  nfdm  4911  nfres  4949  resmptf  4997  nfiotadw  5223  dffun6f  5272  dffun6  5273  dffun4f  5275  nffun  5282  funimaexglem  5342  nffv  5571  nffvmpt1  5572  dffn5imf  5619  funfvdm2f  5629  fvmptss2  5639  fvmpts  5642  fvmpt2  5648  fvmptssdm  5649  mptfvex  5650  fvmptdv  5653  fvmptd3  5658  elfvmptrab1  5659  eqfnfv2f  5666  ralrnmpt  5707  rexrnmpt  5708  f1ompt  5716  ffnfvf  5724  fmptco  5731  fmptcof  5732  fmptcos  5733  funiunfvdmf  5814  dff13f  5820  f1mpt  5821  fliftfuns  5848  nfiso  5856  nfriotadxy  5889  csbriotag  5893  riota2  5903  mpoeq123  5985  cbvmpox  6004  cbvmpo  6005  cbvmpov  6006  ovmpos  6050  ov2gf  6051  ovmpodxf  6052  ovmpodx  6053  ovmpodv  6059  ovmpodv2  6060  fvmpopr2d  6063  ovi3  6064  elovmporab  6127  elovmporab1w  6128  nfof  6145  nfofr  6146  offval2  6155  ofrfval2  6156  abrexex2g  6186  abrexex2  6190  uchoice  6204  dfopab2  6256  dfoprab3s  6257  mpomptsx  6264  dmmpossx  6266  fmpox  6267  mpofvex  6272  fnmpoovd  6282  fmpoco  6283  dfmpo  6290  f1od2  6302  disjxp1  6303  mpoxopoveq  6307  mpoxopovel  6308  nftpos  6346  tposoprab  6347  nfrecs  6374  nffrec  6463  eqerlem  6632  qliftfuns  6687  cbvixpv  6784  nfixpxy  6785  nfixp1  6786  ixpf  6788  mptelixpg  6802  dom2lem  6840  xpcomco  6894  xpf1o  6914  mapxpen  6918  ac6sfi  6968  opabfi  7008  nfsup  7067  nfdju  7117  exmidomni  7217  ismkvnex  7230  cc2  7352  cc4f  7354  cc4  7355  caucvgprprlemaddq  7794  caucvgsrlemgt1  7881  axpre-suploclemres  7987  lble  8993  supinfneg  9688  infsupneg  9689  fzrevral  10199  zsupcllemstep  10338  infssuzex  10342  infssuzcldc  10344  nfseq  10568  seq3f1olemstep  10625  seq3f1olemp  10626  nfwrd  10982  fimaxre2  11411  nfsum1  11540  nfsum  11541  cbvsumv  11545  cbvsumi  11546  sumfct  11558  sumrbdclem  11561  summodclem2a  11565  zsumdc  11568  fsum3  11571  isumss  11575  isumss2  11577  fsum3cvg2  11578  fsumzcl2  11589  fsumadd  11590  fsumsplitf  11592  sumsnf  11593  sumsn  11595  sumsns  11599  fsumsplitsnun  11603  fsum2dlemstep  11618  fisumcom2  11622  fsumshftm  11629  fsum00  11646  fsumrelem  11655  fsumiun  11661  mertenslem2  11720  prodeq1  11737  nfcprod1  11738  nfcprod  11739  cbvprod  11742  cbvprodv  11743  cbvprodi  11744  prodrbdclem  11755  prodmodclem2a  11760  zproddc  11763  fprodseq  11767  fprodntrivap  11768  prodfct  11771  prodssdc  11773  prodsnf  11776  prodsn  11777  fprodm1s  11785  fprodp1s  11786  prodsns  11787  fprodcllemf  11797  fprodconst  11804  fprodap0  11805  fprod2dlemstep  11806  fprodcom2fi  11810  fprodrec  11813  fproddivapf  11815  fprodsplitf  11816  fprodap0f  11820  fprodle  11824  bezoutlemmain  12192  bezout  12205  nnwofdc  12232  nnwosdc  12233  prmind2  12315  oddpwdclemdvds  12365  oddpwdclemndvds  12366  pcmpt  12539  pcmptdvds  12541  ctiunctlemudc  12681  ctiunctlemf  12682  ctiunctlemfo  12683  ctiunct  12684  ctiunctal  12685  prdsbas3  12991  gsumfzconstf  13550  cnmpt11  14627  cnmpt1t  14629  cnmpt21  14635  cnmpt2t  14637  cnmptcom  14642  imasnopn  14643  fsumcncntop  14911  ellimc3apf  15004  ellimc3ap  15005  limcmpted  15007  dvmptfsum  15069  elplyd  15085  fsumdvdsmul  15335  lgseisenlem2  15420  elabf1  15535  elabf2  15536  elabg2  15539  bj-omssind  15689  bj-bdfindisg  15702  bj-nntrans  15705  bj-nnelirr  15707  bj-omtrans  15710  setindis  15721  bdsetindis  15723  bj-nn0sucALT  15732  bj-findis  15733  bj-findisg  15734  strcollnfALT  15740  isomninnlem  15787  trilpolemeq1  15797  trirec0  15801  iswomninnlem  15806  ismkvnnlem  15809  nconstwlpolemgt0  15821