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  4004  cbviinv  4005  ssiun2s  4009  iunab  4012  ssiinf  4015  ssiin  4016  iinab  4027  cbvdisjv  4070  nfdisjv  4071  disjnims  4074  disji2  4075  invdisjrab  4077  cbvmptv  4180  triun  4195  csbexga  4212  repizf2  4246  moop2  4338  euotd  4341  opelopabgf  4358  opelopabf  4363  nfpo  4392  nfso  4393  pofun  4403  nfse  4432  nffrfor  4439  nffr  4440  frind  4443  nfwe  4446  eusvnf  4544  rabxfrd  4560  tfis  4675  tfisi  4679  opeliunxp  4774  nfrel  4804  opeliunxp2  4862  ralxpf  4868  rexxpf  4869  nfco  4887  nfcnv  4901  dfdmf  4916  dfrnf  4965  nfdm  4968  nfres  5007  resmptf  5055  nfiotadw  5281  dffun6f  5331  dffun6  5332  dffun4f  5334  nffun  5341  funimaexglem  5404  nffv  5639  nffvmpt1  5640  dffn5imf  5691  funfvdm2f  5701  fvmptss2  5711  fvmpts  5714  fvmpt2  5720  fvmptssdm  5721  mptfvex  5722  fvmptdv  5725  fvmptd3  5730  elfvmptrab1  5731  eqfnfv2f  5738  ralrnmpt  5779  rexrnmpt  5780  f1ompt  5788  ffnfvf  5796  fmptco  5803  fmptcof  5804  fmptcos  5805  funiunfvdmf  5894  dff13f  5900  f1mpt  5901  fliftfuns  5928  nfiso  5936  nfriotadxy  5969  csbriotag  5974  riota2  5984  mpoeq123  6069  cbvmpox  6088  cbvmpo  6089  cbvmpov  6090  ovmpos  6134  ov2gf  6135  ovmpodxf  6136  ovmpodx  6137  ovmpodv  6143  ovmpodv2  6144  fvmpopr2d  6147  ovi3  6148  elovmporab  6211  elovmporab1w  6212  nfof  6230  nfofr  6231  offval2  6240  ofrfval2  6241  abrexex2g  6271  abrexex2  6275  uchoice  6289  dfopab2  6341  dfoprab3s  6342  mpomptsx  6349  dmmpossx  6351  fmpox  6352  mpofvex  6357  fnmpoovd  6367  fmpoco  6368  dfmpo  6375  f1od2  6387  disjxp1  6388  mpoxopoveq  6392  mpoxopovel  6393  nftpos  6431  tposoprab  6432  nfrecs  6459  nffrec  6548  eqerlem  6719  qliftfuns  6774  cbvixpv  6871  nfixpxy  6872  nfixp1  6873  ixpf  6875  mptelixpg  6889  dom2lem  6931  xpcomco  6993  xpf1o  7013  mapxpen  7017  ac6sfi  7068  opabfi  7111  nfsup  7170  nfdju  7220  exmidomni  7320  ismkvnex  7333  cc2  7464  cc4f  7466  cc4  7467  caucvgprprlemaddq  7906  caucvgsrlemgt1  7993  axpre-suploclemres  8099  lble  9105  supinfneg  9802  infsupneg  9803  fzrevral  10313  zsupcllemstep  10461  infssuzex  10465  infssuzcldc  10467  nfseq  10691  seq3f1olemstep  10748  seq3f1olemp  10749  nfwrd  11113  reuccatpfxs1v  11295  fimaxre2  11753  nfsum1  11882  nfsum  11883  cbvsumv  11887  cbvsumi  11888  sumfct  11900  sumrbdclem  11903  summodclem2a  11907  zsumdc  11910  fsum3  11913  isumss  11917  isumss2  11919  fsum3cvg2  11920  fsumzcl2  11931  fsumadd  11932  fsumsplitf  11934  sumsnf  11935  sumsn  11937  sumsns  11941  fsumsplitsnun  11945  fsum2dlemstep  11960  fisumcom2  11964  fsumshftm  11971  fsum00  11988  fsumrelem  11997  fsumiun  12003  mertenslem2  12062  prodeq1  12079  nfcprod1  12080  nfcprod  12081  cbvprod  12084  cbvprodv  12085  cbvprodi  12086  prodrbdclem  12097  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  fprodntrivap  12110  prodfct  12113  prodssdc  12115  prodsnf  12118  prodsn  12119  fprodm1s  12127  fprodp1s  12128  prodsns  12129  fprodcllemf  12139  fprodconst  12146  fprodap0  12147  fprod2dlemstep  12148  fprodcom2fi  12152  fprodrec  12155  fproddivapf  12157  fprodsplitf  12158  fprodap0f  12162  fprodle  12166  bezoutlemmain  12534  bezout  12547  nnwofdc  12574  nnwosdc  12575  prmind2  12657  oddpwdclemdvds  12707  oddpwdclemndvds  12708  pcmpt  12881  pcmptdvds  12883  ctiunctlemudc  13023  ctiunctlemf  13024  ctiunctlemfo  13025  ctiunct  13026  ctiunctal  13027  prdsbas3  13335  gsumfzconstf  13894  cnmpt11  14972  cnmpt1t  14974  cnmpt21  14980  cnmpt2t  14982  cnmptcom  14987  imasnopn  14988  fsumcncntop  15256  ellimc3apf  15349  ellimc3ap  15350  limcmpted  15352  dvmptfsum  15414  elplyd  15430  fsumdvdsmul  15680  lgseisenlem2  15765  gropd  15863  grstructd2dom  15864  lfgrnloopen  15946  elabf1  16200  elabf2  16201  elabg2  16204  bj-omssind  16353  bj-bdfindisg  16366  bj-nntrans  16369  bj-nnelirr  16371  bj-omtrans  16374  setindis  16385  bdsetindis  16387  bj-nn0sucALT  16396  bj-findis  16397  bj-findisg  16398  strcollnfALT  16404  isomninnlem  16458  trilpolemeq1  16468  trirec0  16472  iswomninnlem  16477  ismkvnnlem  16480  nconstwlpolemgt0  16492