Theorem nfcv 2374

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

Syntax hints:   ∈ wcel 2202  Ⅎwnfc 2361

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 1497  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-nfc 2363

This theorem is referenced by:  nfcvd  2375  nfel  2383  nfeq1  2384  nfel1  2385  nfeq2  2386  nfel2  2387  nfcvf  2397  r2al  2551  r2ex  2552  nfraldxy  2565  nfrexdxy  2566  nfra2xy  2574  r19.12  2639  ralcom  2696  rexcom  2697  nfreudxy  2707  raleq  2730  rexeq  2731  reueq1  2732  rmoeq1  2733  cbvralw  2760  cbvrexw  2761  cbvral  2763  cbvrex  2764  rabeq  2794  rabeqi  2795  cbvrabv  2801  vtoclg  2864  vtocl2g  2868  vtoclga  2870  vtocl2ga  2872  vtocl3ga  2874  spcimdv  2890  spcimedv  2892  spcgv  2893  spcegv  2894  rspct  2903  rspc  2904  rspce  2905  rspc2  2921  ceqsexg  2934  elabgt  2947  elabf  2949  elabg  2952  elab3g  2957  elrab  2962  mob  2988  nfsbc1v  3050  elrabsf  3070  sbcralt  3108  sbcrext  3109  sbcralg  3110  sbcrex  3111  sbcreug  3112  reu8nf  3113  cbvcsbv  3133  csbconstg  3141  nfcsb1v  3160  csbie  3173  csbnestg  3182  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  cbvralv2  3194  cbvrexv2  3195  dfss4st  3440  n0rf  3507  n0r  3508  eq0  3513  raaanlem  3599  nfpw  3665  cbviunv  4009  cbviinv  4010  ssiun2s  4014  iunab  4017  ssiinf  4020  ssiin  4021  iinab  4032  cbvdisjv  4075  nfdisjv  4076  disjnims  4079  disji2  4080  invdisjrab  4082  cbvmptv  4185  triun  4200  csbexga  4217  repizf2  4252  moop2  4344  euotd  4347  opelopabgf  4364  opelopabf  4369  nfpo  4398  nfso  4399  pofun  4409  nfse  4438  nffrfor  4445  nffr  4446  frind  4449  nfwe  4452  eusvnf  4550  rabxfrd  4566  tfis  4681  tfisi  4685  opeliunxp  4781  nfrel  4811  opeliunxp2  4870  ralxpf  4876  rexxpf  4877  nfco  4895  nfcnv  4909  dfdmf  4924  dfrnf  4973  nfdm  4976  nfres  5015  resmptf  5063  nfiotadw  5289  dffun6f  5339  dffun6  5340  dffun4f  5342  nffun  5349  funimaexglem  5413  nffv  5649  nffvmpt1  5650  dffn5imf  5701  funfvdm2f  5711  fvmptss2  5721  fvmpts  5724  fvmpt2  5730  fvmptssdm  5731  mptfvex  5732  fvmptdv  5735  fvmptd3  5740  elfvmptrab1  5741  eqfnfv2f  5748  ralrnmpt  5789  rexrnmpt  5790  f1ompt  5798  ffnfvf  5806  fmptco  5813  fmptcof  5814  fmptcos  5815  funiunfvdmf  5904  dff13f  5910  f1mpt  5911  fliftfuns  5938  nfiso  5946  nfriotadxy  5979  csbriotag  5984  riota2  5994  mpoeq123  6079  cbvmpox  6098  cbvmpo  6099  cbvmpov  6100  ovmpos  6144  ov2gf  6145  ovmpodxf  6146  ovmpodx  6147  ovmpodv  6153  ovmpodv2  6154  fvmpopr2d  6157  ovi3  6158  elovmporab  6221  elovmporab1w  6222  nfof  6240  nfofr  6241  offval2  6250  ofrfval2  6251  abrexex2g  6281  abrexex2  6285  uchoice  6299  dfopab2  6351  dfoprab3s  6352  mpomptsx  6361  dmmpossx  6363  fmpox  6364  mpofvex  6369  fnmpoovd  6379  fmpoco  6380  dfmpo  6387  f1od2  6399  disjxp1  6400  mpoxopoveq  6405  mpoxopovel  6406  nftpos  6444  tposoprab  6445  nfrecs  6472  nffrec  6561  eqerlem  6732  qliftfuns  6787  cbvixpv  6884  nfixpxy  6885  nfixp1  6886  ixpf  6888  mptelixpg  6902  dom2lem  6944  modom  6993  xpcomco  7009  xpf1o  7029  mapxpen  7033  ac6sfi  7086  opabfi  7131  nfsup  7190  nfdju  7240  exmidomni  7340  ismkvnex  7353  cc2  7485  cc4f  7487  cc4  7488  caucvgprprlemaddq  7927  caucvgsrlemgt1  8014  axpre-suploclemres  8120  lble  9126  supinfneg  9828  infsupneg  9829  fzrevral  10339  zsupcllemstep  10488  infssuzex  10492  infssuzcldc  10494  nfseq  10718  seq3f1olemstep  10775  seq3f1olemp  10776  nfwrd  11141  reuccatpfxs1v  11328  fimaxre2  11787  nfsum1  11916  nfsum  11917  cbvsumv  11921  cbvsumi  11922  sumfct  11934  sumrbdclem  11937  summodclem2a  11941  zsumdc  11944  fsum3  11947  isumss  11951  isumss2  11953  fsum3cvg2  11954  fsumzcl2  11965  fsumadd  11966  fsumsplitf  11968  sumsnf  11969  sumsn  11971  sumsns  11975  fsumsplitsnun  11979  fsum2dlemstep  11994  fisumcom2  11998  fsumshftm  12005  fsum00  12022  fsumrelem  12031  fsumiun  12037  mertenslem2  12096  prodeq1  12113  nfcprod1  12114  nfcprod  12115  cbvprod  12118  cbvprodv  12119  cbvprodi  12120  prodrbdclem  12131  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  fprodntrivap  12144  prodfct  12147  prodssdc  12149  prodsnf  12152  prodsn  12153  fprodm1s  12161  fprodp1s  12162  prodsns  12163  fprodcllemf  12173  fprodconst  12180  fprodap0  12181  fprod2dlemstep  12182  fprodcom2fi  12186  fprodrec  12189  fproddivapf  12191  fprodsplitf  12192  fprodap0f  12196  fprodle  12200  bezoutlemmain  12568  bezout  12581  nnwofdc  12608  nnwosdc  12609  prmind2  12691  oddpwdclemdvds  12741  oddpwdclemndvds  12742  pcmpt  12915  pcmptdvds  12917  ctiunctlemudc  13057  ctiunctlemf  13058  ctiunctlemfo  13059  ctiunct  13060  ctiunctal  13061  prdsbas3  13369  gsumfzconstf  13928  cnmpt11  15006  cnmpt1t  15008  cnmpt21  15014  cnmpt2t  15016  cnmptcom  15021  imasnopn  15022  fsumcncntop  15290  ellimc3apf  15383  ellimc3ap  15384  limcmpted  15386  dvmptfsum  15448  elplyd  15464  fsumdvdsmul  15714  lgseisenlem2  15799  gropd  15897  grstructd2dom  15898  lfgrnloopen  15983  elabf1  16377  elabf2  16378  elabg2  16381  bj-omssind  16530  bj-bdfindisg  16543  bj-nntrans  16546  bj-nnelirr  16548  bj-omtrans  16551  setindis  16562  bdsetindis  16564  bj-nn0sucALT  16573  bj-findis  16574  bj-findisg  16575  strcollnfALT  16581  isomninnlem  16634  trilpolemeq1  16644  trirec0  16648  iswomninnlem  16653  ismkvnnlem  16656  nconstwlpolemgt0  16668