Theorem nfcv 2372

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

Syntax hints:   ∈ wcel 2200  Ⅎwnfc 2359

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 1495  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-nfc 2361

This theorem is referenced by:  nfcvd  2373  nfel  2381  nfeq1  2382  nfel1  2383  nfeq2  2384  nfel2  2385  nfcvf  2395  r2al  2549  r2ex  2550  nfraldxy  2563  nfrexdxy  2564  nfra2xy  2572  r19.12  2637  ralcom  2694  rexcom  2695  nfreudxy  2705  raleq  2728  rexeq  2729  reueq1  2730  rmoeq1  2731  cbvralw  2758  cbvrexw  2759  cbvral  2761  cbvrex  2762  rabeq  2791  rabeqi  2792  cbvrabv  2798  vtoclg  2861  vtocl2g  2865  vtoclga  2867  vtocl2ga  2869  vtocl3ga  2871  spcimdv  2887  spcimedv  2889  spcgv  2890  spcegv  2891  rspct  2900  rspc  2901  rspce  2902  rspc2  2918  ceqsexg  2931  elabgt  2944  elabf  2946  elabg  2949  elab3g  2954  elrab  2959  mob  2985  nfsbc1v  3047  elrabsf  3067  sbcralt  3105  sbcrext  3106  sbcralg  3107  sbcrex  3108  sbcreug  3109  reu8nf  3110  cbvcsbv  3130  csbconstg  3138  nfcsb1v  3157  csbie  3170  csbnestg  3179  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  cbvralv2  3191  cbvrexv2  3192  dfss4st  3437  n0rf  3504  n0r  3505  eq0  3510  raaanlem  3596  nfpw  3662  cbviunv  4003  cbviinv  4004  ssiun2s  4008  iunab  4011  ssiinf  4014  ssiin  4015  iinab  4026  cbvdisjv  4069  nfdisjv  4070  disjnims  4073  disji2  4074  invdisjrab  4076  cbvmptv  4179  triun  4194  csbexga  4211  repizf2  4245  moop2  4337  euotd  4340  opelopabgf  4357  opelopabf  4362  nfpo  4391  nfso  4392  pofun  4402  nfse  4431  nffrfor  4438  nffr  4439  frind  4442  nfwe  4445  eusvnf  4543  rabxfrd  4559  tfis  4674  tfisi  4678  opeliunxp  4773  nfrel  4803  opeliunxp2  4861  ralxpf  4867  rexxpf  4868  nfco  4886  nfcnv  4900  dfdmf  4915  dfrnf  4964  nfdm  4967  nfres  5006  resmptf  5054  nfiotadw  5280  dffun6f  5330  dffun6  5331  dffun4f  5333  nffun  5340  funimaexglem  5403  nffv  5636  nffvmpt1  5637  dffn5imf  5688  funfvdm2f  5698  fvmptss2  5708  fvmpts  5711  fvmpt2  5717  fvmptssdm  5718  mptfvex  5719  fvmptdv  5722  fvmptd3  5727  elfvmptrab1  5728  eqfnfv2f  5735  ralrnmpt  5776  rexrnmpt  5777  f1ompt  5785  ffnfvf  5793  fmptco  5800  fmptcof  5801  fmptcos  5802  funiunfvdmf  5887  dff13f  5893  f1mpt  5894  fliftfuns  5921  nfiso  5929  nfriotadxy  5962  csbriotag  5967  riota2  5977  mpoeq123  6062  cbvmpox  6081  cbvmpo  6082  cbvmpov  6083  ovmpos  6127  ov2gf  6128  ovmpodxf  6129  ovmpodx  6130  ovmpodv  6136  ovmpodv2  6137  fvmpopr2d  6140  ovi3  6141  elovmporab  6204  elovmporab1w  6205  nfof  6222  nfofr  6223  offval2  6232  ofrfval2  6233  abrexex2g  6263  abrexex2  6267  uchoice  6281  dfopab2  6333  dfoprab3s  6334  mpomptsx  6341  dmmpossx  6343  fmpox  6344  mpofvex  6349  fnmpoovd  6359  fmpoco  6360  dfmpo  6367  f1od2  6379  disjxp1  6380  mpoxopoveq  6384  mpoxopovel  6385  nftpos  6423  tposoprab  6424  nfrecs  6451  nffrec  6540  eqerlem  6709  qliftfuns  6764  cbvixpv  6861  nfixpxy  6862  nfixp1  6863  ixpf  6865  mptelixpg  6879  dom2lem  6921  xpcomco  6981  xpf1o  7001  mapxpen  7005  ac6sfi  7056  opabfi  7096  nfsup  7155  nfdju  7205  exmidomni  7305  ismkvnex  7318  cc2  7449  cc4f  7451  cc4  7452  caucvgprprlemaddq  7891  caucvgsrlemgt1  7978  axpre-suploclemres  8084  lble  9090  supinfneg  9786  infsupneg  9787  fzrevral  10297  zsupcllemstep  10444  infssuzex  10448  infssuzcldc  10450  nfseq  10674  seq3f1olemstep  10731  seq3f1olemp  10732  nfwrd  11095  reuccatpfxs1v  11275  fimaxre2  11733  nfsum1  11862  nfsum  11863  cbvsumv  11867  cbvsumi  11868  sumfct  11880  sumrbdclem  11883  summodclem2a  11887  zsumdc  11890  fsum3  11893  isumss  11897  isumss2  11899  fsum3cvg2  11900  fsumzcl2  11911  fsumadd  11912  fsumsplitf  11914  sumsnf  11915  sumsn  11917  sumsns  11921  fsumsplitsnun  11925  fsum2dlemstep  11940  fisumcom2  11944  fsumshftm  11951  fsum00  11968  fsumrelem  11977  fsumiun  11983  mertenslem2  12042  prodeq1  12059  nfcprod1  12060  nfcprod  12061  cbvprod  12064  cbvprodv  12065  cbvprodi  12066  prodrbdclem  12077  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  fprodntrivap  12090  prodfct  12093  prodssdc  12095  prodsnf  12098  prodsn  12099  fprodm1s  12107  fprodp1s  12108  prodsns  12109  fprodcllemf  12119  fprodconst  12126  fprodap0  12127  fprod2dlemstep  12128  fprodcom2fi  12132  fprodrec  12135  fproddivapf  12137  fprodsplitf  12138  fprodap0f  12142  fprodle  12146  bezoutlemmain  12514  bezout  12527  nnwofdc  12554  nnwosdc  12555  prmind2  12637  oddpwdclemdvds  12687  oddpwdclemndvds  12688  pcmpt  12861  pcmptdvds  12863  ctiunctlemudc  13003  ctiunctlemf  13004  ctiunctlemfo  13005  ctiunct  13006  ctiunctal  13007  prdsbas3  13315  gsumfzconstf  13874  cnmpt11  14951  cnmpt1t  14953  cnmpt21  14959  cnmpt2t  14961  cnmptcom  14966  imasnopn  14967  fsumcncntop  15235  ellimc3apf  15328  ellimc3ap  15329  limcmpted  15331  dvmptfsum  15393  elplyd  15409  fsumdvdsmul  15659  lgseisenlem2  15744  gropd  15842  grstructd2dom  15843  lfgrnloopen  15925  elabf1  16103  elabf2  16104  elabg2  16107  bj-omssind  16256  bj-bdfindisg  16269  bj-nntrans  16272  bj-nnelirr  16274  bj-omtrans  16277  setindis  16288  bdsetindis  16290  bj-nn0sucALT  16299  bj-findis  16300  bj-findisg  16301  strcollnfALT  16307  isomninnlem  16357  trilpolemeq1  16367  trirec0  16371  iswomninnlem  16376  ismkvnnlem  16379  nconstwlpolemgt0  16391