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

Theorem nfcv 2582
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 1751 . 2  |-  F/ x  y  e.  A
21nfci 2571 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1867   F/_wnfc 2568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-5 1748
This theorem depends on definitions:  df-bi 188  df-nf 1664  df-nfc 2570
This theorem is referenced by:  nfcvd  2583  nfelOLD  2596  nfeq1  2597  nfel1  2598  nfeq2  2599  nfel2  2600  nfcvf  2607  r2alOLD  2802  nfra2  2810  r2exOLD  2950  r19.12  2952  ralcom  2987  rexcom  2988  raleq  3023  rexeq  3024  reueq1  3025  rmoeq1  3026  cbvral  3049  cbvrex  3050  rabeq  3072  cbvrabv  3077  vtocl2g  3140  vtoclga  3142  vtocl2ga  3144  vtocl3ga  3146  spcimdv  3160  spcgv  3163  spcegv  3164  rspct  3172  rspc  3173  rspce  3174  rspc2  3187  elabgt  3212  elabf  3214  elabg  3216  elab3g  3221  elrab  3226  2rmorex  3273  nfsbc1v  3316  elrabsf  3335  sbcralt  3369  sbcralg  3371  sbcrex  3372  sbcreu  3373  cbvcsbv  3398  csbconstg  3405  nfcsb1v  3408  csbie  3418  cbvralcsf  3424  cbvreucsf  3426  cbvrabcsf  3427  cbvralv2  3428  cbvrexv2  3429  n0f  3767  n0  3768  csbnestg  3812  raaan  3902  nfpw  3988  nfop  4197  rabasiun  4297  cbviunv  4332  cbviinv  4333  ssiun2s  4337  iunab  4339  ssiinf  4342  ssiin  4343  iinab  4354  cbvdisjv  4399  disjors  4403  disji2  4404  invdisjrab  4407  disjprg  4413  disjxiun  4414  disjxun  4415  cbvmptv  4509  triun  4524  zfrep3cl  4536  csbexg  4550  eusvnf  4611  reusv2lem4  4620  reusv2  4622  rabxfrd  4634  moop2  4707  euotd  4713  opelopabgf  4732  opelopabf  4737  nfpo  4771  nfso  4772  pofun  4782  nffr  4819  nfse  4820  opeliunxp  4897  nfrel  4931  ralxpf  4992  nfco  5011  nfcnv  5024  dfdmf  5039  dfrnf  5084  nfdm  5087  nfres  5118  wfisg  5425  dffun6f  5606  dffun6  5607  nffun  5614  nffv  5879  nffvmpt1  5880  dffn5f  5927  funfv2f  5941  fvmpt2f  5956  fvmpts  5958  fvmpt2i  5963  fvmptss  5965  fvmptex  5967  fvmptdv  5969  fvmptnf  5974  fvmptn  5975  elfvmptrab1  5977  fvopab5  5980  eqfnfv2f  5986  ralrnmpt  6037  f1ompt  6050  ffnfvf  6056  fmptco  6062  fmptcof  6063  fmptcos  6064  funiunfvf  6160  dff13f  6166  f1mpt  6168  fliftfuns  6213  nfiso  6221  csbriota  6270  riota2  6280  riotaxfrd  6288  oprabv  6344  mpt2eq123  6355  cbvmpt2x  6374  cbvmpt2  6375  cbvmpt2v  6376  ovmpt2s  6425  ov2gf  6426  ovmpt2dxf  6427  ovmpt2dx  6428  ovmpt2dv  6434  ovmpt2dv2  6435  ov3  6438  elovmpt2rab  6520  elovmpt2rab1  6521  ovmpt3rab1  6530  ovmpt3rabdm  6531  elovmpt3rab1  6532  nfof  6541  nfofr  6542  offval2f  6548  offval2  6553  ofrfval2  6554  ofmpteq  6555  onminesb  6630  onminsb  6631  tfis  6686  tfisi  6690  zfrep6  6766  abrexex2g  6775  abrexex2  6779  dfopab2  6852  dfoprab3s  6853  mpt2mptsx  6861  dmmpt2ssx  6863  fmpt2x  6864  fnmpt2ovd  6876  offval22  6877  ovmptss  6879  fmpt2co  6881  dfmpt2  6888  mpt2xopoveq  6964  mpt2xopovel  6965  nftpos  7007  tposoprab  7008  mpt2curryd  7015  mpt2curryvald  7016  fvmpt2curryd  7017  nfwrecs  7029  nfrecs  7092  nfrdg  7131  rdgsucmpt2  7147  rdgsucmpt  7148  frsucmpt  7154  frsucmptn  7155  frsucmpt2  7156  oawordeulem  7254  nnawordex  7337  qliftfuns  7449  cbvixpv  7539  nfixp  7540  nfixp1  7541  ixpf  7543  mptelixpg  7558  dom2lem  7607  xpcomco  7659  xpf1o  7731  mapxpen  7735  ac6sfi  7812  iunfi  7859  indexfi  7879  dffi3  7942  nfoi  8020  ixpiunwdom  8097  cantnflem1  8184  cnfcomlem  8194  r1val1  8247  rankidb  8261  rankval4  8328  scottex  8346  scottexs  8348  scott0s  8349  cp  8352  tskwe  8374  cardmin2  8422  fseqenlem1  8444  dfac8clem  8452  cardaleph  8509  hsmexlem2  8846  axcc2  8856  ac6num  8898  ac6c4  8900  axdclem  8938  iundom2g  8954  uniimadomf  8959  cardmin  8978  pwfseqlem2  9073  pwfseqlem4a  9075  pwfseqlem4  9076  inar1  9189  lble  10547  nnwof  11214  nnwos  11215  fzrevral  11866  rabssnn0fi  12184  nfseq  12209  seqof2  12257  hashrabsn1  12539  nfwrd  12671  relexpsucnnr  13056  rlim2  13527  ello1mpt  13552  rlimcld2  13609  o1compt  13618  nfsum1  13723  nfsum  13724  sumeq2ii  13726  cbvsumv  13729  cbvsumi  13730  sumfc  13742  summolem2a  13748  zsum  13751  sumss  13757  sumss2  13759  fsumcvg2  13760  fsumzcl2  13771  fsumadd  13772  sumsn  13774  sumsns  13778  fsummsnunz  13782  fsumsplitsnun  13783  fsum2dlem  13798  fsumcom2  13802  fsumshftm  13809  fsummulc2  13812  fsum00  13825  fsumrelem  13834  fsumrlim  13838  fsumo1  13839  o1fsum  13840  fsumiun  13848  prodeq1  13930  nfcprod1  13931  nfcprod  13932  cbvprod  13936  cbvprodv  13937  cbvprodi  13938  prodmolem2a  13955  zprod  13958  fprod  13962  fprodntriv  13963  prodfc  13966  prodss  13968  fprodcllemf  13979  fprodmul  13981  fproddiv  13982  prodsn  13983  prodsnf  13985  fprodm1s  13991  fprodp1s  13992  prodsns  13993  fprodn0  14000  fprod2dlem  14001  fprodcom2  14005  fproddivf  14008  fprodsplitf  14009  fprodsplit1f  14011  fprodle  14017  fprodefsum  14116  prmind2  14595  coprmprod  14638  coprmproddvdslem  14639  pcmpt  14789  pcmptdvds  14791  prdsbas3  15331  prdsdsval2  15334  mreiincl  15446  invfuc  15823  yonedalem4b  16105  gsumconstf  17496  gsumsnd  17513  gsumsn  17515  gsumunsnd  17518  gsummpt1n0  17525  gsum2d2lem  17533  gsum2d2  17534  gsumcom2  17535  prdsgsum  17538  dprd2d2  17605  gsumdixp  17765  lss1d  18114  psrass1lem  18529  evlslem4  18659  mpfrcl  18669  coe1fzgsumdlem  18823  gsummoncoe1  18826  gsumply1eq  18827  evl1gsumdlem  18872  mdetralt2  19558  mdetunilem2  19562  madugsum  19592  gsummatr01lem4  19607  cayleyhamilton1  19840  neiptopnei  20072  fiuncmp  20343  iuncon  20367  2ndcdisj  20395  dissnlocfin  20468  elptr2  20513  ptbasfi  20520  ptunimpt  20534  ptcldmpt  20553  ptclsg  20554  ptcnplem  20560  ptcnp  20561  cnmpt11  20602  cnmpt1t  20604  cnmpt21  20610  cnmpt2t  20612  cnmptcom  20617  cnmptk2  20625  cnmpt2k  20627  imasnopn  20629  imasncld  20630  imasncls  20631  xkocnv  20753  elmptrab  20766  flfcnp2  20946  ptcmpg  20996  fmucnd  21231  prdsdsf  21306  prdsxmet  21308  cfilucfil  21498  blval2  21501  restmetu  21509  fsumcn  21791  fsum2cn  21792  ovolfiniun  22328  ovoliunlem3  22331  ovoliun  22332  ovoliun2  22333  ovoliunnul  22334  finiunmbl  22371  volfiniun  22374  iundisj  22375  iundisj2  22376  iunmbl  22380  voliun  22381  iunmbl2  22384  mbfpos  22481  mbfposr  22482  mbfposb  22483  mbfsup  22494  mbfinf  22495  mbfinfOLD  22496  mbflim  22500  i1fposd  22539  itg1climres  22546  itg2splitlem  22580  itg2split  22581  itg2cnlem1  22593  isibl2  22598  itgeq1  22604  nfitg1  22605  nfitg  22606  cbvitg  22607  cbvitgv  22608  itgmpt  22614  itgss3  22646  itgfsum  22658  itgabs  22666  itggt0  22673  itgcn  22674  cbvditgv  22684  limcmpt  22712  limciun  22723  dvmptfsum  22801  dvlipcn  22820  lhop2  22841  dvfsumle  22847  dvfsumabs  22849  dvfsumlem1  22852  dvfsumlem2  22853  dvfsumlem4  22855  dvfsumrlim  22857  dvfsum2  22860  itgparts  22873  itgsubstlem  22874  itgsubst  22875  elplyd  23021  coeeq2  23061  dgrle  23062  ulmss  23214  itgulm2  23226  leibpi  23730  rlimcnp  23753  rlimcnp2  23754  o1cxp  23762  lgamgulmlem2  23817  lgamgulmlem6  23821  lgamgulm2  23823  fsumdvdscom  23974  fsumdvdsmul  23984  fsumvma  24001  lgseisenlem2  24138  dchrisumlema  24186  dchrisumlem2  24188  dchrisumlem3  24189  nbgraopALT  24994  cnlnadjlem5  27556  chirred  27880  vtocl2d  27941  ralcom4f  27942  rexcom4f  27943  rmo4fOLD  27964  rabtru  27968  iunin1f  28007  iunxsngf  28008  iunxdif3  28011  disji2f  28023  disjorsf  28026  disjif2  28027  disjabrex  28028  disjabrexf  28029  iundisjf  28035  iundisj2f  28036  disjunsn  28040  dfrel4  28044  ac6sf2  28063  dfimafnf  28070  suppss2fOLD  28074  suppss2f  28075  fimarab  28081  fmptdF  28092  resmptf  28094  feqmptdf  28095  fmptcof2  28096  fcomptf  28097  acunirnmpt2  28099  acunirnmpt2f  28100  aciunf1lem  28101  aciunf1  28102  ofpreima  28105  funcnvmptOLD  28107  funcnvmpt  28108  funcnv5mpt  28109  funcnv4mpt  28110  f1od2  28149  fpwrelmap  28158  fpwrelmapffs  28159  xrofsup  28186  iundisjfi  28205  iundisj2fi  28206  iundisjcnt  28207  iundisj2cnt  28208  nnindf  28217  gsummpt2co  28378  gsumvsca1  28381  gsumvsca2  28382  mdetpmtr1  28485  ordtconlem1  28566  qqhval2  28622  esumcl  28687  nfesum1  28697  nfesum2  28698  cbvesumv  28700  esumid  28701  esumgsum  28702  esumval  28703  esumel  28704  esumnul  28705  esumc  28708  esumrnmpt  28709  esumsplit  28710  esummono  28711  esumpad  28712  esumpad2  28713  esumadd  28714  esumle  28715  gsumesum  28716  esumlub  28717  esumaddf  28718  esumsnf  28721  esumsn  28722  esumpr  28723  esumrnmpt2  28725  esumfzf  28726  esumfsup  28727  esumss  28729  esumpinfval  28730  esumpfinvalf  28733  esumpinfsum  28734  esumpcvgval  28735  esumpmono  28736  esumcocn  28737  esummulc1  28738  esummulc2  28739  esumdivc  28740  esumcvg  28743  esumsup  28746  esumgect  28747  esum2dlem  28749  esum2d  28750  esumiun  28751  sigaclcu2  28778  ldsysgenld  28818  sigapildsys  28820  ldgenpisyslem1  28821  fiunelros  28832  measvunilem  28870  measvunilem0  28871  measvuni  28872  measiuns  28875  measiun  28876  meascnbl  28877  voliune  28888  volfiniune  28889  volmeas  28890  ddemeas  28895  imambfm  28920  omscl  28953  oms0  28955  omsmon  28956  omssubadd  28958  carsgclctunlem1  28975  carsggect  28976  carsgclctunlem2  28977  omsmeas  28981  sibfof  28998  eulerpartlemn  29037  bnj23  29309  bnj1366  29426  bnj1400  29432  bnj1534  29449  bnj1542  29453  bnj607  29512  bnj873  29520  bnj958  29536  bnj1000  29537  bnj981  29546  bnj1014  29556  bnj1123  29580  bnj1204  29606  bnj1388  29627  bnj1398  29628  bnj1408  29630  bnj1445  29638  bnj1446  29639  bnj1447  29640  bnj1448  29641  bnj1449  29642  bnj1466  29647  bnj1467  29648  bnj1463  29649  bnj1312  29652  bnj1498  29655  bnj1519  29659  bnj1520  29660  bnj1525  29663  bnj1529  29664  cvmcov  29771  setinds  30208  dfon2lem3  30215  tfisg  30241  trpredlem1  30252  trpredtr  30255  trpredmintr  30256  trpred0  30261  trpredrec  30263  frinsg  30267  nfwlim  30289  sltval2  30327  nobndlem5  30367  finminlem  30756  bj-rabtrALT  31281  topdifinfindis  31480  topdifinffinlem  31481  isbasisrelowllem1  31489  isbasisrelowllem2  31490  iooelexlt  31496  relowlssretop  31497  phpreu  31633  finixpnum  31634  ptrest  31643  poimirlem16  31660  poimirlem19  31663  poimirlem23  31667  poimirlem24  31668  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  poimirlem28  31672  mbfposadd  31692  dvtanlemOLD  31695  itgabsnc  31715  itggt0cn  31718  ftc1cnnclem  31719  ftc1anclem5  31725  ftc2nc  31730  indexa  31764  indexdom  31765  filbcmb  31771  sdclem2  31775  sdclem1  31776  fdc1  31779  totbndbnd  31825  heibor1  31846  scottexf  32115  scott0f  32116  ac6s6f  32120  fsumshftd  32232  fsumshftdOLD  32233  riotasvd  32237  riotasv2d  32238  riotasv2s  32239  riotaocN  32484  cdleme26ee  33636  cdleme31sn1  33657  cdleme31se2  33659  cdlemefrs29bpre0  33672  cdlemefs32sn1aw  33690  cdleme43fsv1snlem  33696  cdleme41sn3a  33709  cdleme32d  33720  cdleme32f  33722  cdleme40m  33743  cdleme40n  33744  cdleme42b  33754  ltrniotaval  33857  cdlemksv2  34123  cdlemkuv2  34143  cdlemk36  34189  cdlemk38  34191  cdlemkid  34212  cdlemk19x  34219  cdlemk11t  34222  dihglblem5  34575  hlhilset  35214  elrfirn2  35247  mzpsubst  35299  eq0rabdioph  35328  sbcrexgOLD  35337  sbccomieg  35345  rexrabdioph  35346  rexfrabdioph  35347  rabdiophlem2  35354  elnn0rabdioph  35355  dvdsrabdioph  35362  rabrenfdioph  35366  monotoddzz  35501  oddcomabszz  35502  setindtrs  35590  wdom2d2  35600  aomclem6  35627  aomclem8  35629  areaquad  35804  ss2iundv  35895  cbviuneq12dv  35897  binomcxplemdvbinom  36343  binomcxplemdvsum  36345  binomcxplemnotnn0  36346  compab  36435  iunconlem2  36976  evth2f  36980  elunif  36981  fvelrnbf  36983  rfcnpre1  36984  fsumcnf  36986  sumsnd  36991  evthf  36992  refsumcn  36995  rfcnpre2  36996  rfcnpre3  36998  rfcnpre4  36999  rfcnnnub  37001  refsum2cnlem1  37002  refsum2cn  37003  uzwo4  37037  iunxsngf2  37048  fiiuncl  37052  suprnmpt  37065  dffo3f  37077  elrnmptf  37081  disjf1  37084  wessf1ornlem  37086  disjrnmpt2  37090  disjf1o  37093  fompt  37094  disjinfi  37095  ssfiunibd  37140  supxrgere  37169  iuneqfzuzlem  37170  supxrgelem  37173  supxrge  37174  fsumclf  37224  fsumsplitf  37225  fsummulc1f  37226  sumsnf  37227  fsumsplit1  37230  fsumf1of  37232  fsumiunss  37233  fmul01  37234  fmuldfeqlem1  37236  fmuldfeq  37237  fmul01lt1lem1  37238  fmul01lt1lem2  37239  fmul01lt1  37240  cncfmptss  37241  mulc1cncfg  37243  infrglbOLD  37245  expcnfg  37247  fprodexp  37250  fprodabs2  37251  mccllem  37253  mccl  37254  climmulf  37258  climexp  37259  climsuse  37263  climrecf  37264  climinff  37266  climinffOLD  37267  climaddf  37271  mullimc  37272  constlimc  37280  idlimc  37282  limcperiod  37284  sumnnodd  37286  neglimc  37304  addlimc  37305  0ellimcdiv  37306  cncfshift  37327  icccncfext  37341  cncficcgt0  37342  cncfiooicclem1  37347  fprodcncf  37355  dvcosre  37357  dvmptmulf  37385  dvnmptdivc  37386  dvnmul  37391  dvmptfprodlem  37392  dvmptfprod  37393  dvnprodlem1  37394  dvnprodlem2  37395  itgsin0pilem1  37399  ibliccsinexp  37400  itgsinexplem1  37403  itgsinexp  37404  iblsplitf  37420  itgsubsticclem  37425  stoweidlem3  37436  stoweidlem14  37447  stoweidlem16  37449  stoweidlem18  37451  stoweidlem21  37454  stoweidlem23  37456  stoweidlem26  37459  stoweidlem27  37460  stoweidlem28  37461  stoweidlem29  37462  stoweidlem29OLD  37463  stoweidlem31  37465  stoweidlem34  37468  stoweidlem35  37469  stoweidlem36  37470  stoweidlem41  37475  stoweidlem42  37476  stoweidlem43  37477  stoweidlem46  37480  stoweidlem47  37481  stoweidlem48  37482  stoweidlem51  37485  stoweidlem52  37486  stoweidlem53  37487  stoweidlem54  37488  stoweidlem55  37489  stoweidlem56  37490  stoweidlem57  37491  stoweidlem58  37492  stoweidlem59  37493  stoweidlem60  37494  stoweidlem62  37496  stoweidlem62OLD  37497  stowei  37499  wallispilem5  37504  stirlinglem4  37512  stirlinglem5  37513  stirlinglem11  37519  stirlinglem12  37520  stirlinglem13  37521  stirlinglem14  37522  stirlinglem15  37523  stirling  37524  fourierdlem20  37562  fourierdlem31  37573  fourierdlem48  37590  fourierdlem51  37593  fourierdlem68  37610  fourierdlem73  37615  fourierdlem79  37621  fourierdlem80  37622  fourierdlem86  37628  fourierdlem89  37631  fourierdlem91  37633  fourierdlem103  37645  fourierdlem104  37646  fourierdlem112  37654  fourierdlem115  37657  fourierd  37658  fourierclimd  37659  etransclem2  37672  etransclem24  37694  etransclem25  37695  etransclem26  37696  etransclem28  37698  etransclem32  37702  etransclem35  37705  etransclem37  37707  etransclem44  37714  etransclem46  37716  etransclem48  37718  sge00  37756  sge0revalmpt  37758  sge0f1o  37762  sge0fsummpt  37770  sge0pnffigt  37776  sge0lefi  37778  sge0ltfirp  37780  sge0resplit  37786  sge0lempt  37790  sge0iunmptlemfi  37793  sge0iunmptlemre  37795  sge0fodjrnlem  37796  sge0iunmpt  37798  iundjiun  37811  meadjiun  37817  omeiunle  37851  omeiunltfirp  37853  carageniuncllem1  37855  caratheodorylem1  37860  caratheodorylem2  37861  cbvral2  37997  cbvrex2  37998  raaan2  38000  2reurex  38006  2reu3  38013  2reu7  38016  2reu8  38017  eu2ndop1stv  38027  nfafv  38041  fsummsndifre  38428  fsumsplitsndif  38429  fsummmodsndifre  38430  fsummmodsnunz  38431  opeliun2xp  38887  dmmpt2ssx2  38891  ovmpt2rdxf  38893  ovmpt2rdx  38894  aacllem  39314
  Copyright terms: Public domain W3C validator