Theorem nfcv 2392

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

This proof depends on syntax axioms:   ∈ wcel 2209  Ⅎwnfc 2379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-nfc 2381

This theorem is used by:  nfcvd  2393  nfel  2401  nfeq1  2402  nfel1  2403  nfeq2  2404  nfel2  2405  nfcvf  2415  r2al  2569  r2ex  2570  nfraldxy  2583  nfrexdxy  2584  nfra2xy  2592  r19.12  2657  ralcom  2714  rexcom  2715  nfreudxy  2725  raleq  2749  rexeq  2750  reueq1  2751  rmoeq1  2752  cbvralw  2779  cbvrexw  2780  cbvral  2782  cbvrex  2783  rabeq  2813  rabeqi  2814  cbvrabv  2820  vtoclg  2883  vtocl2g  2887  vtoclga  2889  vtocl2ga  2891  vtocl3ga  2893  spcimdv  2909  spcimedv  2911  spcgv  2912  spcegv  2913  rspct  2922  rspc  2923  rspce  2924  rspc2  2941  ceqsexg  2954  elabgt  2967  elabf  2969  elabg  2972  elab3g  2977  elrab  2982  mob  3008  nfsbc1v  3070  elrabsf  3090  sbcralt  3128  sbcrext  3129  sbcralg  3130  sbcrex  3131  sbcreug  3132  reu8nf  3133  cbvcsbv  3153  csbconstg  3161  nfcsb1v  3180  csbie  3193  csbnestg  3202  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  cbvralv2  3214  cbvrexv2  3215  dfss4st  3464  n0rf  3534  n0r  3535  eq0  3540  raaanlem  3632  nfpw  3705  cbviunv  4051  cbviinv  4052  ssiun2s  4056  iunab  4059  ssiinf  4062  ssiin  4063  iinab  4074  cbvdisjv  4117  nfdisjv  4118  disjnims  4121  disji2  4122  invdisjrab  4124  cbvmptv  4229  triun  4244  csbexga  4263  repizf2  4301  moop2  4394  euotd  4397  opelopabgf  4414  opelopabf  4419  nfpo  4448  nfso  4449  pofun  4459  nfse  4488  nffrfor  4495  nffr  4496  frind  4499  nfwe  4502  eusvnf  4601  rabxfrd  4617  tfis  4732  tfisi  4736  opeliunxp  4832  nfrel  4862  opeliunxp2  4922  ralxpf  4928  rexxpf  4929  nfco  4947  nfcnv  4961  dfdmf  4976  dfrnf  5025  nfdm  5028  nfres  5067  resmptf  5116  nfiotadw  5343  dffun6f  5393  dffun6  5394  dffun4f  5396  nffun  5403  funimaexglem  5467  nffv  5708  nffvmpt1  5709  dffn5imf  5761  funfvdm2f  5771  fvmptss2  5783  fvmpts  5786  fvmpt2  5792  fvmptssdm  5793  mptfvex  5794  fvmptdv  5797  fvmptd3  5802  elfvmptrab1  5804  eqfnfv2f  5813  ralrnmpt  5853  rexrnmpt  5854  f1ompt  5862  ffnfvf  5870  fmptco  5877  fmptcof  5878  fmptcos  5879  dfimafnf  5958  funiunfvdmf  5973  dff13f  5979  f1mpt  5980  fliftfuns  6007  nfiso  6015  nfriotadxy  6050  csbriotag  6055  riota2  6065  mpoeq123  6150  cbvmpox  6169  cbvmpo  6170  cbvmpov  6171  ovmpos  6215  ov2gf  6216  ovmpodxf  6217  ovmpodx  6218  ovmpodv  6224  ovmpodv2  6225  fvmpopr2d  6228  ovi3  6229  elovmporab  6292  elovmporab1w  6293  nfof  6312  nfofr  6313  offval2  6322  ofrfval2  6323  abrexex2g  6353  abrexex2  6357  uchoice  6375  dfopab2  6427  dfoprab3s  6428  mpomptsx  6437  dmmpossx  6439  fmpox  6440  mpofvex  6445  fnmpoovd  6455  fmpoco  6456  dfmpo  6463  f1od2  6475  disjxp1  6476  mpoxopoveq  6515  mpoxopovel  6516  nftpos  6554  tposoprab  6555  nfrecs  6582  nffrec  6671  eqerlem  6842  qliftfuns  6897  cbvixpv  7002  nfixpxy  7003  nfixp1  7004  ixpf  7006  mptelixpg  7020  dom2lem  7062  modom  7112  xpcomco  7128  xpf1o  7148  mapxpen  7152  ac6sfi  7206  opabfi  7251  nfsup  7338  nfdju  7388  exmidomni  7488  ismkvnex  7501  cc2  7639  cc4f  7641  cc4  7642  caucvgprprlemaddq  8081  caucvgsrlemgt1  8168  axpre-suploclemres  8274  lble  9285  supinfneg  10011  infsupneg  10012  fzrevral  10529  zsupcllemstep  10679  infssuzex  10683  infssuzcldc  10685  infssfzcldc  10686  infssfzledc  10687  nfseq  10915  seq3f1olemstep  10972  seq3f1olemp  10973  nfwrd  11355  reuccatpfxs1v  11542  fimaxre2  12016  nfsum1  12147  nfsum  12148  cbvsumv  12152  cbvsumi  12153  sumfct  12165  sumrbdclem  12169  summodclem2a  12173  zsumdc  12176  fsum3  12179  isumss  12183  isumss2  12185  fsum3cvg2  12186  fsumzcl2  12197  fsumadd  12198  fsumsplitf  12200  sumsnf  12201  sumsn  12203  sumsns  12207  fsumsplitsnun  12211  fsum2dlemstep  12226  fisumcom2  12230  fsumshftm  12237  fsum00  12254  fsumrelem  12263  fsumiun  12269  mertenslem2  12328  prodeq1  12345  nfcprod1  12346  nfcprod  12347  cbvprod  12350  cbvprodv  12351  cbvprodi  12352  prodrbdclem  12363  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  fprodntrivap  12376  prodfct  12379  prodssdc  12381  prodsnf  12384  prodsn  12385  fprodm1s  12393  fprodp1s  12394  prodsns  12395  fprodcllemf  12405  fprodconst  12412  fprodap0  12413  fprod2dlemstep  12414  fprodcom2fi  12418  fprodrec  12421  fproddivapf  12423  fprodsplitf  12424  fprodap0f  12428  fprodle  12432  bezoutlemmain  12800  bezout  12813  nnwofdc  12840  nnwosdc  12841  prmind2  12923  nnmaxpwlemdvds  12974  nnmaxpwlemndvds  12975  pcmpt  13151  pcmptdvds  13153  ctiunctlemudc  13386  ctiunctlemf  13387  ctiunctlemfo  13388  ctiunct  13389  ctiunctal  13390  gzsumconstf  14234  gzsumsplit0  14238  gsumsncmn  14246  gsummptfidmadd  14251  gsumsnfdcmn  14257  gsumsndcmn  14258  gsumunsnd  14260  gsum2d2fi  14274  gsumcom2fi  14275  prdsbas3  14294  psrass1filem  15177  cnmpt11  15509  cnmpt1t  15511  cnmpt21  15517  cnmpt2t  15519  cnmptcom  15524  imasnopn  15525  fsumcncntop  15793  ellimc3apf  15886  ellimc3ap  15887  limcmpted  15889  dvmptfsum  15951  elplyd  15967  fsumdvdsmul  16285  lgseisenlem2  16395  gropd  16493  grstructd2dom  16494  lfgrnloopen  16579  elabf1  17014  elabf2  17015  elabg2  17018  bj-omssind  17166  bj-bdfindisg  17179  bj-nntrans  17182  bj-nnelirr  17184  bj-omtrans  17187  setindis  17198  bdsetindis  17200  bj-nn0sucALT  17209  bj-findis  17210  bj-findisg  17211  strcollnfALT  17217  isomninnlem  17285  trilpolemeq1  17296  trirec0  17300  iswomninnlem  17306  ismkvnnlem  17309  nconstwlpolemgt0  17321