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

Theorem nfcv 2619
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.
StepHypRef Expression
1 nfv 1707 . 2
21nfci 2608 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  F/_wnfc 2605
This theorem is referenced by:  nfcvd  2620  nfelOLD  2633  nfeq1  2634  nfel1  2635  nfeq2  2636  nfel2  2637  nfcvf  2644  r2alOLD  2836  nfra2  2844  r2exOLD  2981  r19.12  2983  ralcom  3018  rexcom  3019  raleq  3054  rexeq  3055  reueq1  3056  rmoeq1  3057  cbvral  3080  cbvrex  3081  rabeq  3103  cbvrabv  3108  vtocl2g  3171  vtoclga  3173  vtocl2ga  3175  vtocl3ga  3177  spcimdv  3191  spcgv  3194  spcegv  3195  rspct  3203  rspc  3204  rspce  3205  rspc2  3218  elabgt  3243  elabf  3245  elabg  3247  elab3g  3252  elrab  3257  2rmorex  3304  nfsbc1v  3347  elrabsf  3366  sbcralt  3408  sbcralg  3411  sbcrex  3412  sbcrexgOLD  3413  sbcreu  3414  sbcreugOLD  3415  cbvcsbv  3440  csbconstg  3447  nfcsb1v  3450  csbie  3460  cbvralcsf  3466  cbvreucsf  3468  cbvrabcsf  3469  cbvralv2  3470  cbvrexv2  3471  n0f  3793  n0  3794  csbnestg  3842  raaan  3937  nfpw  4024  nfop  4233  rabasiun  4334  cbviunv  4369  cbviinv  4370  ssiun2s  4374  iunab  4376  ssiinf  4379  ssiin  4380  iinab  4391  cbvdisjv  4433  disjors  4438  disji2  4439  disjprg  4448  disjxiun  4449  disjxun  4450  cbvmptv  4543  triun  4558  zfrep3cl  4570  csbexg  4584  csbexgOLD  4586  eusvnf  4647  reusv2lem4  4656  reusv2  4658  reusv6OLD  4663  rabxfrd  4673  moop2  4747  euotd  4753  opelopabgf  4772  opelopabf  4777  nfpo  4810  nfso  4811  pofun  4821  nffr  4858  nfse  4859  opeliunxp  5056  nfrel  5093  ralxpf  5154  nfco  5173  nfcnv  5186  dfdmf  5201  dfrnf  5246  nfdm  5249  nfres  5280  dffun6f  5607  dffun6  5608  nffun  5615  nffv  5878  nffvmpt1  5879  dffn5f  5928  funfv2f  5942  fvmpts  5958  fvmpt2i  5962  fvmptss  5964  fvmptex  5966  fvmptdv  5968  fvmptnf  5973  fvmptn  5974  elfvmptrab1  5976  fvopab5  5979  eqfnfv2f  5985  ralrnmpt  6040  f1ompt  6053  ffnfvf  6058  fmptco  6064  fmptcof  6065  fmptcos  6066  funiunfvf  6161  dff13f  6167  f1mpt  6169  fliftfuns  6212  nfiso  6220  csbriota  6269  riota2  6280  riotaxfrd  6288  oprabv  6345  mpt2eq123  6356  cbvmpt2x  6375  cbvmpt2  6376  cbvmpt2v  6377  ovmpt2s  6426  ov2gf  6427  ovmpt2dxf  6428  ovmpt2dx  6429  ovmpt2dv  6435  ovmpt2dv2  6436  ov3  6439  elovmpt2rab  6521  elovmpt2rab1  6522  ovmpt3rab1  6534  ovmpt3rabdm  6535  elovmpt3rab1  6536  nfof  6545  nfofr  6546  offval2  6556  ofrfval2  6557  ofmpteq  6558  onminesb  6633  onminsb  6634  tfis  6689  tfisi  6693  zfrep6  6768  abrexex2g  6777  abrexex2  6781  dfopab2  6854  dfoprab3s  6855  mpt2mptsx  6863  dmmpt2ssx  6865  fmpt2x  6866  fnmpt2ovd  6878  offval22  6879  ovmptss  6881  fmpt2co  6883  dfmpt2  6890  mpt2xopoveq  6966  mpt2xopovel  6967  nftpos  7009  tposoprab  7010  mpt2curryd  7017  mpt2curryvald  7018  fvmpt2curryd  7019  nfrecs  7063  nfrdg  7099  rdgsucmpt2  7115  rdgsucmpt  7116  frsucmpt  7122  frsucmptn  7123  frsucmpt2  7124  oawordeulem  7222  nnawordex  7305  qliftfuns  7417  cbvixpv  7507  nfixp  7508  nfixp1  7509  ixpf  7511  mptelixpg  7526  dom2lem  7575  xpcomco  7627  xpf1o  7699  mapxpen  7703  ac6sfi  7784  iunfi  7828  indexfi  7848  dffi3  7911  nfoi  7960  ixpiunwdom  8038  cantnflem1  8129  cnfcomlem  8164  cnfcomlemOLD  8172  r1val1  8225  rankidb  8239  rankval4  8306  scottex  8324  scottexs  8326  scott0s  8327  cp  8330  tskwe  8352  cardmin2  8400  fseqenlem1  8426  dfac8clem  8434  cardaleph  8491  hsmexlem2  8828  axcc2  8838  ac6num  8880  ac6c4  8882  axdclem  8920  iundom2g  8936  uniimadomf  8941  cardmin  8960  pwfseqlem2  9058  pwfseqlem4a  9060  pwfseqlem4  9061  inar1  9174  lble  10520  nnwof  11177  nnwos  11178  fzrevral  11792  rabssnn0fi  12095  nfseq  12117  seqof2  12165  hashrabsn1  12442  nfwrd  12569  rlim2  13319  ello1mpt  13344  rlimcld2  13401  o1compt  13410  nfsum1  13512  nfsum  13513  sumeq2ii  13515  cbvsumv  13518  cbvsumi  13519  sumfc  13531  summolem2a  13537  zsum  13540  sumss  13546  sumss2  13548  fsumcvg2  13549  fsumzcl2  13560  fsumadd  13561  sumsn  13563  sumsns  13565  fsummsnunz  13569  fsumsplitsnun  13570  fsum2dlem  13585  fsumcom2  13589  fsumshftm  13596  fsummulc2  13599  fsum00  13612  fsumrelem  13621  fsumrlim  13625  fsumo1  13626  o1fsum  13627  fsumiun  13635  prodeq1  13716  nfcprod1  13717  nfcprod  13718  cbvprod  13722  cbvprodv  13723  cbvprodi  13724  prodmolem2a  13741  zprod  13744  fprod  13748  fprodntriv  13749  prodfc  13752  prodss  13754  fprodmul  13765  fproddiv  13766  prodsn  13767  fprodm1s  13774  fprodp1s  13775  prodsns  13776  fprodn0  13783  fprod2dlem  13784  fprodcom2  13788  fprodefsum  13830  prmind2  14228  pcmpt  14411  pcmptdvds  14413  prdsbas3  14878  prdsdsval2  14881  mreiincl  14993  invfuc  15343  yonedalem4b  15545  gsumconstf  16955  gsumsnd  16979  gsumsn  16981  gsumunsnd  16984  gsummpt1n0  16992  gsum2d2lem  17001  gsum2d2  17002  gsumcom2  17003  prdsgsum  17007  prdsgsumOLD  17008  dprd2d2  17093  gsumdixpOLD  17257  gsumdixp  17258  lss1d  17609  psrass1lem  18029  evlslem4OLD  18173  evlslem4  18174  mpfrcl  18187  coe1fzgsumdlem  18343  gsummoncoe1  18346  gsumply1eq  18347  evl1gsumdlem  18392  mdetralt2  19111  mdetunilem2  19115  madugsum  19145  gsummatr01lem4  19160  cayleyhamilton1  19393  neiptopnei  19633  fiuncmp  19904  iuncon  19929  2ndcdisj  19957  dissnlocfin  20030  elptr2  20075  ptbasfi  20082  ptunimpt  20096  ptcldmpt  20115  ptclsg  20116  ptcnplem  20122  ptcnp  20123  cnmpt11  20164  cnmpt1t  20166  cnmpt21  20172  cnmpt2t  20174  cnmptcom  20179  cnmptk2  20187  cnmpt2k  20189  imasnopn  20191  imasncld  20192  imasncls  20193  xkocnv  20315  elmptrab  20328  flfcnp2  20508  ptcmpg  20557  fmucnd  20795  prdsdsf  20870  prdsxmet  20872  cfilucfilOLD  21072  cfilucfil  21073  blval2  21078  restmetu  21090  fsumcn  21374  fsum2cn  21375  ovolfiniun  21912  ovoliunlem3  21915  ovoliun  21916  ovoliun2  21917  ovoliunnul  21918  finiunmbl  21954  volfiniun  21957  iundisj  21958  iundisj2  21959  iunmbl  21963  voliun  21964  iunmbl2  21967  mbfpos  22058  mbfposr  22059  mbfposb  22060  mbfsup  22071  mbfinf  22072  mbflim  22075  i1fposd  22114  itg1climres  22121  itg2splitlem  22155  itg2split  22156  itg2cnlem1  22168  isibl2  22173  itgeq1  22179  nfitg1  22180  nfitg  22181  cbvitg  22182  cbvitgv  22183  itgmpt  22189  itgss3  22221  itgfsum  22233  itgabs  22241  itggt0  22248  itgcn  22249  cbvditgv  22259  limcmpt  22287  limciun  22298  dvmptfsum  22376  dvlipcn  22395  lhop2  22416  dvfsumle  22422  dvfsumabs  22424  dvfsumlem1  22427  dvfsumlem2  22428  dvfsumlem4  22430  dvfsumrlim  22432  dvfsum2  22435  itgparts  22448  itgsubstlem  22449  itgsubst  22450  elplyd  22599  coeeq2  22639  dgrle  22640  ulmss  22792  itgulm2  22804  leibpi  23273  rlimcnp  23295  rlimcnp2  23296  o1cxp  23304  fsumdvdscom  23461  fsumdvdsmul  23471  fsumvma  23488  lgseisenlem2  23625  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  nbgraopALT  24424  cnlnadjlem5  26990  chirred  27314  ralcom4f  27375  rexcom4f  27376  rmo4fOLD  27395  disji2f  27438  disjorsf  27441  disjif2  27442  disjabrex  27443  disjabrexf  27444  iundisjf  27448  iundisj2f  27449  disjunsn  27453  dfrel4  27454  dfimafnf  27473  suppss2f  27477  fimarab  27483  fmptdF  27495  resmptf  27497  fvmpt2f  27498  feqmptdf  27501  fmptcof2  27502  fcomptf  27503  offval2f  27506  ofpreima  27507  funcnvmptOLD  27509  funcnvmpt  27510  funcnv5mpt  27511  funcnv4mpt  27512  f1od2  27547  fpwrelmap  27556  fpwrelmapffs  27557  xrofsup  27582  iundisjfi  27601  iundisj2fi  27602  iundisjcnt  27603  iundisj2cnt  27604  nnindf  27610  gsummpt2co  27771  gsumvsca1  27773  gsumvsca2  27774  ordtconlem1  27906  qqhval2  27963  esumcl  28043  nfesum1  28053  cbvesumv  28055  esumid  28056  esumval  28057  esumel  28058  esumnul  28059  esumsplit  28063  esumadd  28064  esumle  28065  esummono  28066  gsumesum  28067  esumlub  28068  esumaddf  28069  esumpr  28073  esumfzf  28075  esumfsup  28076  esumss  28078  esumpinfval  28079  esumpfinvalf  28082  esumpinfsum  28083  esumpcvgval  28084  esumpmono  28085  esumcocn  28086  esummulc1  28087  esummulc2  28088  esumdivc  28089  esumcvg  28092  sigaclcu2  28120  measvunilem  28183  measvunilem0  28184  measvuni  28185  measiuns  28188  measiun  28189  meascnbl  28190  voliune  28201  volfiniune  28202  volmeas  28203  ddemeas  28208  imambfm  28233  oms0  28266  omsmon  28267  sibfof  28282  eulerpartlemn  28320  lgamgulmlem2  28572  lgamgulmlem6  28576  lgamgulm2  28578  cvmcov  28708  relexpsucr  29053  setinds  29210  dfon2lem3  29217  tfisg  29284  wfisg  29289  trpredlem1  29310  trpredtr  29313  trpredmintr  29314  trpred0  29319  trpredrec  29321  frinsg  29325  nfwrecs  29338  nfwlim  29378  sltval2  29416  nobndlem5  29456  finixpnum  30038  ptrest  30048  mbfposadd  30062  dvtanlem  30064  itgabsnc  30084  itggt0cn  30087  ftc1cnnclem  30088  ftc1anclem5  30094  ftc2nc  30099  finminlem  30136  indexa  30224  indexdom  30225  filbcmb  30231  sdclem2  30235  sdclem1  30236  fdc1  30239  totbndbnd  30285  heibor1  30306  scottexf  30576  scott0f  30577  ac6s6f  30581  elrfirn2  30628  mzpsubst  30681  eq0rabdioph  30710  sbccomieg  30726  rexrabdioph  30727  rexfrabdioph  30728  rabdiophlem2  30735  elnn0rabdioph  30736  dvdsrabdioph  30743  rabrenfdioph  30748  monotoddzz  30879  oddcomabszz  30880  setindtrs  30967  wdom2d2  30977  aomclem6  31005  aomclem8  31007  areaquad  31184  binomcxplemdvbinom  31258  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  compab  31350  evth2f  31390  elunif  31391  fvelrnbf  31393  rfcnpre1  31394  fsumcnf  31396  sumsnd  31401  evthf  31402  refsumcn  31405  rfcnpre2  31406  rfcnpre3  31408  rfcnpre4  31409  rfcnnnub  31411  refsum2cnlem1  31412  refsum2cn  31413  suprnmpt  31451  ssfiunibd  31509  fsumclf  31567  fsumsplitf  31568  fsummulc1f  31569  sumsnf  31570  fsumsplit1  31573  fmul01  31574  fmuldfeqlem1  31576  fmuldfeq  31577  fmul01lt1lem1  31578  fmul01lt1lem2  31579  fmul01lt1  31580  cncfmptss  31581  mulc1cncfg  31583  infrglb  31584  expcnfg  31586  prodsnf  31587  fproddivf  31588  fprodsplitf  31589  fprodcllemf  31591  fprodsplit1f  31593  fprodexp  31600  fprodabs2  31602  fprodle  31604  mccllem  31605  mccl  31606  climmulf  31610  climexp  31611  climsuse  31614  climrecf  31615  climinff  31617  climaddf  31621  mullimc  31622  constlimc  31630  idlimc  31632  limcperiod  31634  sumnnodd  31636  neglimc  31653  addlimc  31654  0ellimcdiv  31655  cncfshift  31676  icccncfext  31690  cncficcgt0  31691  cncfiooicclem1  31696  fprodcncf  31704  dvcosre  31706  dvmptmulf  31734  dvnmptdivc  31735  dvnmul  31740  dvmptfprodlem  31741  dvmptfprod  31742  dvnprodlem1  31743  dvnprodlem2  31744  itgsin0pilem1  31748  ibliccsinexp  31749  itgsinexplem1  31752  itgsinexp  31753  iblsplitf  31769  itgsubsticclem  31774  stoweidlem3  31785  stoweidlem14  31796  stoweidlem16  31798  stoweidlem18  31800  stoweidlem21  31803  stoweidlem23  31805  stoweidlem26  31808  stoweidlem27  31809  stoweidlem28  31810  stoweidlem29  31811  stoweidlem31  31813  stoweidlem34  31816  stoweidlem35  31817  stoweidlem36  31818  stoweidlem41  31823  stoweidlem42  31824  stoweidlem43  31825  stoweidlem46  31828  stoweidlem47  31829  stoweidlem48  31830  stoweidlem51  31833  stoweidlem52  31834  stoweidlem53  31835  stoweidlem54  31836  stoweidlem55  31837  stoweidlem56  31838  stoweidlem57  31839  stoweidlem58  31840  stoweidlem59  31841  stoweidlem60  31842  stoweidlem62  31844  stowei  31846  wallispilem5  31851  stirlinglem4  31859  stirlinglem5  31860  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  stirlinglem14  31869  stirlinglem15  31870  stirling  31871  fourierdlem20  31909  fourierdlem31  31920  fourierdlem48  31937  fourierdlem51  31940  fourierdlem68  31957  fourierdlem73  31962  fourierdlem79  31968  fourierdlem80  31969  fourierdlem86  31975  fourierdlem89  31978  fourierdlem91  31980  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem115  32004  fourierd  32005  fourierclimd  32006  etransclem2  32019  etransclem24  32041  etransclem25  32042  etransclem26  32043  etransclem28  32045  etransclem32  32049  etransclem35  32052  etransclem37  32054  etransclem44  32061  etransclem46  32063  etransclem48  32065  cbvral2  32177  cbvrex2  32178  raaan2  32180  2reurex  32186  2reu3  32193  2reu7  32196  2reu8  32197  eu2ndop1stv  32207  nfafv  32221  fsummsndifre  32345  fsumsplitsndif  32346  fsummmodsndifre  32347  fsummmodsnunz  32348  opeliun2xp  32922  dmmpt2ssx2  32926  ovmpt2rdxf  32928  ovmpt2rdx  32929  aacllem  33216  iunconlem2  33735  bnj23  33771  bnj1366  33888  bnj1400  33894  bnj1534  33911  bnj1542  33915  bnj607  33974  bnj873  33982  bnj958  33998  bnj1000  33999  bnj981  34008  bnj1014  34018  bnj1123  34042  bnj1204  34068  bnj1388  34089  bnj1398  34090  bnj1408  34092  bnj1445  34100  bnj1446  34101  bnj1447  34102  bnj1448  34103  bnj1449  34104  bnj1466  34109  bnj1467  34110  bnj1463  34111  bnj1312  34114  bnj1498  34117  bnj1519  34121  bnj1520  34122  bnj1525  34125  bnj1529  34126  bj-rabtrALT  34498  fsumshftd  34682  fsumshftdOLD  34683  riotasvd  34687  riotasv2d  34688  riotasv2s  34689  riotaocN  34934  cdleme26ee  36086  cdleme31sn1  36107  cdleme31se2  36109  cdlemefrs29bpre0  36122  cdlemefs32sn1aw  36140  cdleme43fsv1snlem  36146  cdleme41sn3a  36159  cdleme32d  36170  cdleme32f  36172  cdleme40m  36193  cdleme40n  36194  cdleme42b  36204  ltrniotaval  36307  cdlemksv2  36573  cdlemkuv2  36593  cdlemk36  36639  cdlemk38  36641  cdlemkid  36662  cdlemk19x  36669  cdlemk11t  36672  dihglblem5  37025  hlhilset  37664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-nf 1617  df-nfc 2607
  Copyright terms: Public domain W3C validator