MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcv Structured version   Unicode version

Theorem nfcv 2603
Description: If  x is disjoint from  A, then  x is not free in  A. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfcv  |-  F/_ x A
Distinct variable group:    x, A

Proof of Theorem nfcv
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 nfv 1692 . 2  |-  F/ x  y  e.  A
21nfci 2592 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1802   F/_wnfc 2589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-5 1689
This theorem depends on definitions:  df-bi 185  df-nf 1602  df-nfc 2591
This theorem is referenced by:  nfcvd  2604  nfelOLD  2617  nfeq1  2618  nfel1  2619  nfeq2  2620  nfel2  2621  nfcvf  2628  r2alOLD  2820  nfra2  2828  r2exOLD  2965  r19.12  2967  ralcom  3002  rexcom  3003  raleq  3038  rexeq  3039  reueq1  3040  rmoeq1  3041  cbvral  3064  cbvrex  3065  rabeq  3087  cbvrabv  3092  vtocl2g  3155  vtoclga  3157  vtocl2ga  3159  vtocl3ga  3161  spcimdv  3175  spcgv  3178  spcegv  3179  rspct  3187  rspc  3188  rspce  3189  rspc2  3202  elabgt  3227  elabf  3229  elabg  3231  elab3g  3236  elrab  3241  2rmorex  3288  nfsbc1v  3331  elrabsf  3350  sbcralt  3392  sbcralg  3395  sbcrex  3396  sbcrexgOLD  3397  sbcreu  3398  sbcreugOLD  3399  cbvcsbv  3424  csbconstg  3431  nfcsb1v  3434  csbie  3444  cbvralcsf  3450  cbvreucsf  3452  cbvrabcsf  3453  cbvralv2  3454  cbvrexv2  3455  n0f  3776  n0  3777  csbnestg  3825  raaan  3919  nfpw  4006  nfop  4215  rabasiun  4316  cbviunv  4351  cbviinv  4352  ssiun2s  4356  iunab  4358  ssiinf  4361  ssiin  4362  iinab  4373  cbvdisjv  4415  disjors  4420  disji2  4421  disjprg  4430  disjxiun  4431  disjxun  4432  cbvmptv  4525  triun  4540  zfrep3cl  4552  csbexg  4566  csbexgOLD  4568  eusvnf  4629  reusv2lem4  4638  reusv2  4640  reusv6OLD  4645  rabxfrd  4655  moop2  4729  euotd  4735  opelopabgf  4754  opelopabf  4759  nfpo  4792  nfso  4793  pofun  4803  nffr  4840  nfse  4841  opeliunxp  5038  nfrel  5075  ralxpf  5136  nfco  5155  nfcnv  5168  dfdmf  5183  dfrnf  5228  nfdm  5231  nfres  5262  dffun6f  5589  dffun6  5590  nffun  5597  nffv  5860  nffvmpt1  5861  dffn5f  5910  funfv2f  5924  fvmpts  5940  fvmpt2i  5944  fvmptss  5946  fvmptex  5948  fvmptdv  5950  fvmptnf  5955  fvmptn  5956  elfvmptrab1  5958  fvopab5  5961  eqfnfv2f  5967  ralrnmpt  6022  f1ompt  6035  ffnfvf  6040  fmptco  6046  fmptcof  6047  fmptcos  6048  funiunfvf  6143  dff13f  6149  f1mpt  6151  fliftfuns  6194  nfiso  6202  csbriota  6251  riota2  6262  riotaxfrd  6270  oprabv  6327  mpt2eq123  6338  cbvmpt2x  6357  cbvmpt2  6358  cbvmpt2v  6359  ovmpt2s  6408  ov2gf  6409  ovmpt2dxf  6410  ovmpt2dx  6411  ovmpt2dv  6417  ovmpt2dv2  6418  ov3  6421  elovmpt2rab  6503  elovmpt2rab1  6504  ovmpt3rab1  6516  ovmpt3rabdm  6517  elovmpt3rab1  6518  nfof  6527  nfofr  6528  offval2  6538  ofrfval2  6539  ofmpteq  6540  onminesb  6615  onminsb  6616  tfis  6671  tfisi  6675  zfrep6  6750  abrexex2g  6759  abrexex2  6763  dfopab2  6836  dfoprab3s  6837  mpt2mptsx  6845  dmmpt2ssx  6847  fmpt2x  6848  fnmpt2ovd  6860  offval22  6861  ovmptss  6863  fmpt2co  6865  dfmpt2  6872  mpt2xopoveq  6946  mpt2xopovel  6947  nftpos  6989  tposoprab  6990  mpt2curryd  6997  mpt2curryvald  6998  fvmpt2curryd  6999  nfrecs  7043  nfrdg  7079  rdgsucmpt2  7095  rdgsucmpt  7096  frsucmpt  7102  frsucmptn  7103  frsucmpt2  7104  oawordeulem  7202  nnawordex  7285  qliftfuns  7397  cbvixpv  7486  nfixp  7487  nfixp1  7488  ixpf  7490  mptelixpg  7505  dom2lem  7554  xpcomco  7606  xpf1o  7678  mapxpen  7682  ac6sfi  7763  iunfi  7807  indexfi  7827  dffi3  7890  nfoi  7939  ixpiunwdom  8017  cantnflem1  8108  cnfcomlem  8143  cnfcomlemOLD  8151  r1val1  8204  rankidb  8218  rankval4  8285  scottex  8303  scottexs  8305  scott0s  8306  cp  8309  tskwe  8331  cardmin2  8379  fseqenlem1  8405  dfac8clem  8413  cardaleph  8470  hsmexlem2  8807  axcc2  8817  ac6num  8859  ac6c4  8861  axdclem  8899  iundom2g  8915  uniimadomf  8920  cardmin  8939  pwfseqlem2  9037  pwfseqlem4a  9039  pwfseqlem4  9040  inar1  9153  lble  10498  nnwof  11154  nnwos  11155  fzrevral  11768  rabssnn0fi  12071  nfseq  12093  seqof2  12141  hashrabsn1  12418  nfwrd  12545  rlim2  13295  ello1mpt  13320  rlimcld2  13377  o1compt  13386  nfsum1  13488  nfsum  13489  sumeq2ii  13491  cbvsumv  13494  cbvsumi  13495  sumfc  13507  summolem2a  13513  zsum  13516  sumss  13522  sumss2  13524  fsumcvg2  13525  fsumzcl2  13536  fsumadd  13537  sumsn  13539  sumsns  13541  fsummsnunz  13545  fsumsplitsnun  13546  fsum2dlem  13561  fsumcom2  13565  fsumshftm  13572  fsummulc2  13575  fsum00  13588  fsumrelem  13597  fsumrlim  13601  fsumo1  13602  o1fsum  13603  fsumiun  13611  prmind2  14102  pcmpt  14285  pcmptdvds  14287  prdsbas3  14752  prdsdsval2  14755  mreiincl  14867  invfuc  15214  yonedalem4b  15416  gsumconstf  16826  gsumsnd  16850  gsumsn  16852  gsumunsnd  16855  gsummpt1n0  16863  gsum2d2lem  16872  gsum2d2  16873  gsumcom2  16874  prdsgsum  16878  prdsgsumOLD  16879  dprd2d2  16964  gsumdixpOLD  17128  gsumdixp  17129  lss1d  17480  psrass1lem  17900  evlslem4OLD  18044  evlslem4  18045  mpfrcl  18058  coe1fzgsumdlem  18214  gsummoncoe1  18217  gsumply1eq  18218  evl1gsumdlem  18263  mdetralt2  18981  mdetunilem2  18985  madugsum  19015  gsummatr01lem4  19030  cayleyhamilton1  19263  neiptopnei  19503  fiuncmp  19774  iuncon  19799  2ndcdisj  19827  dissnlocfin  19900  elptr2  19945  ptbasfi  19952  ptunimpt  19966  ptcldmpt  19985  ptclsg  19986  ptcnplem  19992  ptcnp  19993  cnmpt11  20034  cnmpt1t  20036  cnmpt21  20042  cnmpt2t  20044  cnmptcom  20049  cnmptk2  20057  cnmpt2k  20059  imasnopn  20061  imasncld  20062  imasncls  20063  xkocnv  20185  elmptrab  20198  flfcnp2  20378  ptcmpg  20427  fmucnd  20665  prdsdsf  20740  prdsxmet  20742  cfilucfilOLD  20942  cfilucfil  20943  blval2  20948  restmetu  20960  fsumcn  21244  fsum2cn  21245  ovolfiniun  21782  ovoliunlem3  21785  ovoliun  21786  ovoliun2  21787  ovoliunnul  21788  finiunmbl  21824  volfiniun  21827  iundisj  21828  iundisj2  21829  iunmbl  21833  voliun  21834  iunmbl2  21837  mbfpos  21928  mbfposr  21929  mbfposb  21930  mbfsup  21941  mbfinf  21942  mbflim  21945  i1fposd  21984  itg1climres  21991  itg2splitlem  22025  itg2split  22026  itg2cnlem1  22038  isibl2  22043  itgeq1  22049  nfitg1  22050  nfitg  22051  cbvitg  22052  cbvitgv  22053  itgmpt  22059  itgss3  22091  itgfsum  22103  itgabs  22111  itggt0  22118  itgcn  22119  cbvditgv  22129  limcmpt  22157  limciun  22168  dvmptfsum  22246  dvlipcn  22265  lhop2  22286  dvfsumle  22292  dvfsumabs  22294  dvfsumlem1  22297  dvfsumlem2  22298  dvfsumlem4  22300  dvfsumrlim  22302  dvfsum2  22305  itgparts  22318  itgsubstlem  22319  itgsubst  22320  elplyd  22469  coeeq2  22509  dgrle  22510  ulmss  22661  itgulm2  22673  leibpi  23142  rlimcnp  23164  rlimcnp2  23165  o1cxp  23173  fsumdvdscom  23330  fsumdvdsmul  23340  fsumvma  23357  lgseisenlem2  23494  dchrisumlema  23542  dchrisumlem2  23544  dchrisumlem3  23545  nbgraopALT  24293  cnlnadjlem5  26859  chirred  27183  ralcom4f  27244  rexcom4f  27245  rmo4fOLD  27264  disji2f  27307  disjorsf  27310  disjif2  27311  disjabrex  27312  disjabrexf  27313  iundisjf  27317  iundisj2f  27318  disjunsn  27322  dfrel4  27323  dfimafnf  27342  suppss2f  27346  fimarab  27352  fmptdF  27364  resmptf  27366  fvmpt2f  27367  feqmptdf  27370  fmptcof2  27371  fcomptf  27372  offval2f  27375  ofpreima  27376  funcnvmptOLD  27378  funcnvmpt  27379  funcnv5mpt  27380  funcnv4mpt  27381  f1od2  27416  fpwrelmap  27425  fpwrelmapffs  27426  xrofsup  27451  iundisjfi  27470  iundisj2fi  27471  iundisjcnt  27472  iundisj2cnt  27473  nnindf  27480  gsummpt2co  27641  gsumvsca1  27643  gsumvsca2  27644  ordtconlem1  27776  qqhval2  27833  esumcl  27913  nfesum1  27923  cbvesumv  27925  esumid  27926  esumval  27927  esumel  27928  esumnul  27929  esumsplit  27933  esumadd  27934  esumle  27935  esummono  27936  gsumesum  27937  esumlub  27938  esumaddf  27939  esumpr  27943  esumfzf  27945  esumfsup  27946  esumss  27948  esumpinfval  27949  esumpfinvalf  27952  esumpinfsum  27953  esumpcvgval  27954  esumpmono  27955  esumcocn  27956  esummulc1  27957  esummulc2  27958  esumdivc  27959  esumcvg  27962  sigaclcu2  27990  measvunilem  28053  measvunilem0  28054  measvuni  28055  measiuns  28058  measiun  28059  meascnbl  28060  voliune  28071  volfiniune  28072  volmeas  28073  ddemeas  28078  imambfm  28103  oms0  28136  omsmon  28137  sibfof  28152  eulerpartlemn  28190  lgamgulmlem2  28442  lgamgulmlem6  28446  lgamgulm2  28448  cvmcov  28578  relexpsucr  28923  prodeq1  29013  nfcprod1  29014  nfcprod  29015  cbvprod  29019  cbvprodv  29020  cbvprodi  29021  prodmolem2a  29038  zprod  29041  fprod  29045  fprodntriv  29046  prodfc  29049  prodss  29051  fprodmul  29062  fproddiv  29063  prodsn  29064  fprodm1s  29071  fprodp1s  29072  prodsns  29073  fprodefsum  29076  fprodn0  29081  fprod2dlem  29082  fprodcom2  29086  setinds  29182  dfon2lem3  29189  tfisg  29256  wfisg  29261  trpredlem1  29282  trpredtr  29285  trpredmintr  29286  trpred0  29291  trpredrec  29293  frinsg  29297  nfwrecs  29310  nfwlim  29350  sltval2  29388  nobndlem5  29428  finixpnum  30010  ptrest  30020  mbfposadd  30034  dvtanlem  30036  itgabsnc  30056  itggt0cn  30059  ftc1cnnclem  30060  ftc1anclem5  30066  ftc2nc  30071  finminlem  30108  indexa  30196  indexdom  30197  filbcmb  30203  sdclem2  30207  sdclem1  30208  fdc1  30211  totbndbnd  30257  heibor1  30278  scottexf  30548  scott0f  30549  ac6s6f  30553  elrfirn2  30600  mzpsubst  30653  eq0rabdioph  30682  sbccomieg  30698  rexrabdioph  30699  rexfrabdioph  30700  rabdiophlem2  30707  elnn0rabdioph  30708  dvdsrabdioph  30715  rabrenfdioph  30720  monotoddzz  30851  oddcomabszz  30852  setindtrs  30939  wdom2d2  30949  aomclem6  30977  aomclem8  30979  areaquad  31157  compab  31301  evth2f  31341  elunif  31342  fvelrnbf  31344  rfcnpre1  31345  fsumcnf  31347  sumsnd  31352  evthf  31353  refsumcn  31356  rfcnpre2  31357  rfcnpre3  31359  rfcnpre4  31360  rfcnnnub  31362  refsum2cnlem1  31363  refsum2cn  31364  suprnmpt  31401  ssfiunibd  31458  fmul01  31502  fmuldfeqlem1  31504  fmuldfeq  31505  fmul01lt1lem1  31506  fmul01lt1lem2  31507  fmul01lt1  31508  cncfmptss  31509  mulc1cncfg  31511  infrglb  31512  expcnfg  31514  climmulf  31518  climexp  31519  climsuse  31522  climrecf  31523  climinff  31525  climaddf  31529  mullimc  31530  constlimc  31538  idlimc  31540  limcperiod  31542  sumnnodd  31544  neglimc  31561  addlimc  31562  0ellimcdiv  31563  cncfshift  31583  icccncfext  31597  cncficcgt0  31598  cncfiooicclem1  31603  dvcosre  31610  itgsin0pilem1  31638  ibliccsinexp  31639  itgsinexplem1  31642  itgsinexp  31643  iblsplitf  31659  itgsubsticclem  31664  stoweidlem3  31674  stoweidlem14  31685  stoweidlem16  31687  stoweidlem18  31689  stoweidlem21  31692  stoweidlem23  31694  stoweidlem26  31697  stoweidlem27  31698  stoweidlem28  31699  stoweidlem29  31700  stoweidlem31  31702  stoweidlem34  31705  stoweidlem35  31706  stoweidlem36  31707  stoweidlem41  31712  stoweidlem42  31713  stoweidlem43  31714  stoweidlem46  31717  stoweidlem47  31718  stoweidlem48  31719  stoweidlem51  31722  stoweidlem52  31723  stoweidlem53  31724  stoweidlem54  31725  stoweidlem55  31726  stoweidlem56  31727  stoweidlem57  31728  stoweidlem58  31729  stoweidlem59  31730  stoweidlem60  31731  stoweidlem62  31733  stowei  31735  wallispilem5  31740  stirlinglem4  31748  stirlinglem5  31749  stirlinglem11  31755  stirlinglem12  31756  stirlinglem13  31757  stirlinglem14  31758  stirlinglem15  31759  stirling  31760  fourierdlem20  31798  fourierdlem31  31809  fourierdlem48  31826  fourierdlem51  31829  fourierdlem68  31846  fourierdlem73  31851  fourierdlem79  31857  fourierdlem80  31858  fourierdlem86  31864  fourierdlem89  31867  fourierdlem91  31869  fourierdlem103  31881  fourierdlem104  31882  fourierdlem112  31890  fourierdlem115  31893  fourierd  31894  fourierclimd  31895  cbvral2  32015  cbvrex2  32016  raaan2  32018  2reurex  32024  2reu3  32031  2reu7  32034  2reu8  32035  eu2ndop1stv  32045  nfafv  32059  fsummsndifre  32183  fsumsplitsndif  32184  fsummmodsndifre  32185  fsummmodsnunz  32186  opeliun2xp  32650  dmmpt2ssx2  32654  ovmpt2rdxf  32656  ovmpt2rdx  32657  iunconlem2  33463  bnj23  33499  bnj1366  33616  bnj1400  33622  bnj1534  33639  bnj1542  33643  bnj607  33702  bnj873  33710  bnj958  33726  bnj1000  33727  bnj981  33736  bnj1014  33746  bnj1123  33770  bnj1204  33796  bnj1388  33817  bnj1398  33818  bnj1408  33820  bnj1445  33828  bnj1446  33829  bnj1447  33830  bnj1448  33831  bnj1449  33832  bnj1466  33837  bnj1467  33838  bnj1463  33839  bnj1312  33842  bnj1498  33845  bnj1519  33849  bnj1520  33850  bnj1525  33853  bnj1529  33854  bj-rabtrALT  34231  fsumshftd  34405  fsumshftdOLD  34406  riotasvd  34410  riotasv2d  34411  riotasv2s  34412  riotaocN  34657  cdleme26ee  35809  cdleme31sn1  35830  cdleme31se2  35832  cdlemefrs29bpre0  35845  cdlemefs32sn1aw  35863  cdleme43fsv1snlem  35869  cdleme41sn3a  35882  cdleme32d  35893  cdleme32f  35895  cdleme40m  35916  cdleme40n  35917  cdleme42b  35927  ltrniotaval  36030  cdlemksv2  36296  cdlemkuv2  36316  cdlemk36  36362  cdlemk38  36364  cdlemkid  36385  cdlemk19x  36392  cdlemk11t  36395  dihglblem5  36748  hlhilset  37387
  Copyright terms: Public domain W3C validator