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  2792  rabeqi  2793  cbvrabv  2799  vtoclg  2862  vtocl2g  2866  vtoclga  2868  vtocl2ga  2870  vtocl3ga  2872  spcimdv  2888  spcimedv  2890  spcgv  2891  spcegv  2892  rspct  2901  rspc  2902  rspce  2903  rspc2  2919  ceqsexg  2932  elabgt  2945  elabf  2947  elabg  2950  elab3g  2955  elrab  2960  mob  2986  nfsbc1v  3048  elrabsf  3068  sbcralt  3106  sbcrext  3107  sbcralg  3108  sbcrex  3109  sbcreug  3110  reu8nf  3111  cbvcsbv  3131  csbconstg  3139  nfcsb1v  3158  csbie  3171  csbnestg  3180  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  cbvralv2  3192  cbvrexv2  3193  dfss4st  3438  n0rf  3505  n0r  3506  eq0  3511  raaanlem  3597  nfpw  3663  cbviunv  4007  cbviinv  4008  ssiun2s  4012  iunab  4015  ssiinf  4018  ssiin  4019  iinab  4030  cbvdisjv  4073  nfdisjv  4074  disjnims  4077  disji2  4078  invdisjrab  4080  cbvmptv  4183  triun  4198  csbexga  4215  repizf2  4250  moop2  4342  euotd  4345  opelopabgf  4362  opelopabf  4367  nfpo  4396  nfso  4397  pofun  4407  nfse  4436  nffrfor  4443  nffr  4444  frind  4447  nfwe  4450  eusvnf  4548  rabxfrd  4564  tfis  4679  tfisi  4683  opeliunxp  4779  nfrel  4809  opeliunxp2  4868  ralxpf  4874  rexxpf  4875  nfco  4893  nfcnv  4907  dfdmf  4922  dfrnf  4971  nfdm  4974  nfres  5013  resmptf  5061  nfiotadw  5287  dffun6f  5337  dffun6  5338  dffun4f  5340  nffun  5347  funimaexglem  5410  nffv  5645  nffvmpt1  5646  dffn5imf  5697  funfvdm2f  5707  fvmptss2  5717  fvmpts  5720  fvmpt2  5726  fvmptssdm  5727  mptfvex  5728  fvmptdv  5731  fvmptd3  5736  elfvmptrab1  5737  eqfnfv2f  5744  ralrnmpt  5785  rexrnmpt  5786  f1ompt  5794  ffnfvf  5802  fmptco  5809  fmptcof  5810  fmptcos  5811  funiunfvdmf  5900  dff13f  5906  f1mpt  5907  fliftfuns  5934  nfiso  5942  nfriotadxy  5975  csbriotag  5980  riota2  5990  mpoeq123  6075  cbvmpox  6094  cbvmpo  6095  cbvmpov  6096  ovmpos  6140  ov2gf  6141  ovmpodxf  6142  ovmpodx  6143  ovmpodv  6149  ovmpodv2  6150  fvmpopr2d  6153  ovi3  6154  elovmporab  6217  elovmporab1w  6218  nfof  6236  nfofr  6237  offval2  6246  ofrfval2  6247  abrexex2g  6277  abrexex2  6281  uchoice  6295  dfopab2  6347  dfoprab3s  6348  mpomptsx  6357  dmmpossx  6359  fmpox  6360  mpofvex  6365  fnmpoovd  6375  fmpoco  6376  dfmpo  6383  f1od2  6395  disjxp1  6396  mpoxopoveq  6401  mpoxopovel  6402  nftpos  6440  tposoprab  6441  nfrecs  6468  nffrec  6557  eqerlem  6728  qliftfuns  6783  cbvixpv  6880  nfixpxy  6881  nfixp1  6882  ixpf  6884  mptelixpg  6898  dom2lem  6940  modom  6989  xpcomco  7005  xpf1o  7025  mapxpen  7029  ac6sfi  7080  opabfi  7123  nfsup  7182  nfdju  7232  exmidomni  7332  ismkvnex  7345  cc2  7476  cc4f  7478  cc4  7479  caucvgprprlemaddq  7918  caucvgsrlemgt1  8005  axpre-suploclemres  8111  lble  9117  supinfneg  9819  infsupneg  9820  fzrevral  10330  zsupcllemstep  10479  infssuzex  10483  infssuzcldc  10485  nfseq  10709  seq3f1olemstep  10766  seq3f1olemp  10767  nfwrd  11132  reuccatpfxs1v  11319  fimaxre2  11778  nfsum1  11907  nfsum  11908  cbvsumv  11912  cbvsumi  11913  sumfct  11925  sumrbdclem  11928  summodclem2a  11932  zsumdc  11935  fsum3  11938  isumss  11942  isumss2  11944  fsum3cvg2  11945  fsumzcl2  11956  fsumadd  11957  fsumsplitf  11959  sumsnf  11960  sumsn  11962  sumsns  11966  fsumsplitsnun  11970  fsum2dlemstep  11985  fisumcom2  11989  fsumshftm  11996  fsum00  12013  fsumrelem  12022  fsumiun  12028  mertenslem2  12087  prodeq1  12104  nfcprod1  12105  nfcprod  12106  cbvprod  12109  cbvprodv  12110  cbvprodi  12111  prodrbdclem  12122  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  fprodntrivap  12135  prodfct  12138  prodssdc  12140  prodsnf  12143  prodsn  12144  fprodm1s  12152  fprodp1s  12153  prodsns  12154  fprodcllemf  12164  fprodconst  12171  fprodap0  12172  fprod2dlemstep  12173  fprodcom2fi  12177  fprodrec  12180  fproddivapf  12182  fprodsplitf  12183  fprodap0f  12187  fprodle  12191  bezoutlemmain  12559  bezout  12572  nnwofdc  12599  nnwosdc  12600  prmind2  12682  oddpwdclemdvds  12732  oddpwdclemndvds  12733  pcmpt  12906  pcmptdvds  12908  ctiunctlemudc  13048  ctiunctlemf  13049  ctiunctlemfo  13050  ctiunct  13051  ctiunctal  13052  prdsbas3  13360  gsumfzconstf  13919  cnmpt11  14997  cnmpt1t  14999  cnmpt21  15005  cnmpt2t  15007  cnmptcom  15012  imasnopn  15013  fsumcncntop  15281  ellimc3apf  15374  ellimc3ap  15375  limcmpted  15377  dvmptfsum  15439  elplyd  15455  fsumdvdsmul  15705  lgseisenlem2  15790  gropd  15888  grstructd2dom  15889  lfgrnloopen  15972  elabf1  16313  elabf2  16314  elabg2  16317  bj-omssind  16466  bj-bdfindisg  16479  bj-nntrans  16482  bj-nnelirr  16484  bj-omtrans  16487  setindis  16498  bdsetindis  16500  bj-nn0sucALT  16509  bj-findis  16510  bj-findisg  16511  strcollnfALT  16517  isomninnlem  16570  trilpolemeq1  16580  trirec0  16584  iswomninnlem  16589  ismkvnnlem  16592  nconstwlpolemgt0  16604