Theorem nfcv 2349

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 1552	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
2	1	nfci 2339	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   ∈ wcel 2177  Ⅎwnfc 2336

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 1473  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-nfc 2338

This theorem is referenced by:  nfcvd  2350  nfel  2358  nfeq1  2359  nfel1  2360  nfeq2  2361  nfel2  2362  nfcvf  2372  r2al  2526  r2ex  2527  nfraldxy  2540  nfrexdxy  2541  nfra2xy  2549  r19.12  2613  ralcom  2670  rexcom  2671  nfreudxy  2681  raleq  2703  rexeq  2704  reueq1  2705  rmoeq1  2706  cbvralw  2733  cbvrexw  2734  cbvral  2735  cbvrex  2736  rabeq  2765  rabeqi  2766  cbvrabv  2772  vtoclg  2835  vtocl2g  2839  vtoclga  2841  vtocl2ga  2843  vtocl3ga  2845  spcimdv  2861  spcimedv  2863  spcgv  2864  spcegv  2865  rspct  2874  rspc  2875  rspce  2876  rspc2  2892  ceqsexg  2905  elabgt  2918  elabf  2920  elabg  2923  elab3g  2928  elrab  2933  mob  2959  nfsbc1v  3021  elrabsf  3041  sbcralt  3079  sbcrext  3080  sbcralg  3081  sbcrex  3082  sbcreug  3083  cbvcsbv  3103  csbconstg  3111  nfcsb1v  3130  csbie  3143  csbnestg  3152  cbvralcsf  3160  cbvrexcsf  3161  cbvreucsf  3162  cbvrabcsf  3163  cbvralv2  3164  cbvrexv2  3165  dfss4st  3410  n0rf  3477  n0r  3478  eq0  3483  raaanlem  3569  nfpw  3633  cbviunv  3971  cbviinv  3972  ssiun2s  3976  iunab  3979  ssiinf  3982  ssiin  3983  iinab  3994  cbvdisjv  4037  nfdisjv  4038  disjnims  4041  disji2  4042  invdisjrab  4044  cbvmptv  4147  triun  4162  csbexga  4179  repizf2  4213  moop2  4303  euotd  4306  opelopabgf  4323  opelopabf  4328  nfpo  4355  nfso  4356  pofun  4366  nfse  4395  nffrfor  4402  nffr  4403  frind  4406  nfwe  4409  eusvnf  4507  rabxfrd  4523  tfis  4638  tfisi  4642  opeliunxp  4737  nfrel  4767  opeliunxp2  4825  ralxpf  4831  rexxpf  4832  nfco  4850  nfcnv  4864  dfdmf  4879  dfrnf  4927  nfdm  4930  nfres  4969  resmptf  5017  nfiotadw  5243  dffun6f  5292  dffun6  5293  dffun4f  5295  nffun  5302  funimaexglem  5365  nffv  5598  nffvmpt1  5599  dffn5imf  5646  funfvdm2f  5656  fvmptss2  5666  fvmpts  5669  fvmpt2  5675  fvmptssdm  5676  mptfvex  5677  fvmptdv  5680  fvmptd3  5685  elfvmptrab1  5686  eqfnfv2f  5693  ralrnmpt  5734  rexrnmpt  5735  f1ompt  5743  ffnfvf  5751  fmptco  5758  fmptcof  5759  fmptcos  5760  funiunfvdmf  5845  dff13f  5851  f1mpt  5852  fliftfuns  5879  nfiso  5887  nfriotadxy  5920  csbriotag  5924  riota2  5934  mpoeq123  6016  cbvmpox  6035  cbvmpo  6036  cbvmpov  6037  ovmpos  6081  ov2gf  6082  ovmpodxf  6083  ovmpodx  6084  ovmpodv  6090  ovmpodv2  6091  fvmpopr2d  6094  ovi3  6095  elovmporab  6158  elovmporab1w  6159  nfof  6176  nfofr  6177  offval2  6186  ofrfval2  6187  abrexex2g  6217  abrexex2  6221  uchoice  6235  dfopab2  6287  dfoprab3s  6288  mpomptsx  6295  dmmpossx  6297  fmpox  6298  mpofvex  6303  fnmpoovd  6313  fmpoco  6314  dfmpo  6321  f1od2  6333  disjxp1  6334  mpoxopoveq  6338  mpoxopovel  6339  nftpos  6377  tposoprab  6378  nfrecs  6405  nffrec  6494  eqerlem  6663  qliftfuns  6718  cbvixpv  6815  nfixpxy  6816  nfixp1  6817  ixpf  6819  mptelixpg  6833  dom2lem  6875  xpcomco  6935  xpf1o  6955  mapxpen  6959  ac6sfi  7009  opabfi  7049  nfsup  7108  nfdju  7158  exmidomni  7258  ismkvnex  7271  cc2  7394  cc4f  7396  cc4  7397  caucvgprprlemaddq  7836  caucvgsrlemgt1  7923  axpre-suploclemres  8029  lble  9035  supinfneg  9731  infsupneg  9732  fzrevral  10242  zsupcllemstep  10389  infssuzex  10393  infssuzcldc  10395  nfseq  10619  seq3f1olemstep  10676  seq3f1olemp  10677  nfwrd  11039  fimaxre2  11608  nfsum1  11737  nfsum  11738  cbvsumv  11742  cbvsumi  11743  sumfct  11755  sumrbdclem  11758  summodclem2a  11762  zsumdc  11765  fsum3  11768  isumss  11772  isumss2  11774  fsum3cvg2  11775  fsumzcl2  11786  fsumadd  11787  fsumsplitf  11789  sumsnf  11790  sumsn  11792  sumsns  11796  fsumsplitsnun  11800  fsum2dlemstep  11815  fisumcom2  11819  fsumshftm  11826  fsum00  11843  fsumrelem  11852  fsumiun  11858  mertenslem2  11917  prodeq1  11934  nfcprod1  11935  nfcprod  11936  cbvprod  11939  cbvprodv  11940  cbvprodi  11941  prodrbdclem  11952  prodmodclem2a  11957  zproddc  11960  fprodseq  11964  fprodntrivap  11965  prodfct  11968  prodssdc  11970  prodsnf  11973  prodsn  11974  fprodm1s  11982  fprodp1s  11983  prodsns  11984  fprodcllemf  11994  fprodconst  12001  fprodap0  12002  fprod2dlemstep  12003  fprodcom2fi  12007  fprodrec  12010  fproddivapf  12012  fprodsplitf  12013  fprodap0f  12017  fprodle  12021  bezoutlemmain  12389  bezout  12402  nnwofdc  12429  nnwosdc  12430  prmind2  12512  oddpwdclemdvds  12562  oddpwdclemndvds  12563  pcmpt  12736  pcmptdvds  12738  ctiunctlemudc  12878  ctiunctlemf  12879  ctiunctlemfo  12880  ctiunct  12881  ctiunctal  12882  prdsbas3  13189  gsumfzconstf  13748  cnmpt11  14825  cnmpt1t  14827  cnmpt21  14833  cnmpt2t  14835  cnmptcom  14840  imasnopn  14841  fsumcncntop  15109  ellimc3apf  15202  ellimc3ap  15203  limcmpted  15205  dvmptfsum  15267  elplyd  15283  fsumdvdsmul  15533  lgseisenlem2  15618  gropd  15716  grstructd2dom  15717  elabf1  15851  elabf2  15852  elabg2  15855  bj-omssind  16005  bj-bdfindisg  16018  bj-nntrans  16021  bj-nnelirr  16023  bj-omtrans  16026  setindis  16037  bdsetindis  16039  bj-nn0sucALT  16048  bj-findis  16049  bj-findisg  16050  strcollnfALT  16056  isomninnlem  16104  trilpolemeq1  16114  trirec0  16118  iswomninnlem  16123  ismkvnnlem  16126  nconstwlpolemgt0  16138