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

Theorem nfcv 2563
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 1755 . 2  |-  F/ x  y  e.  A
21nfci 2553 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872   F/_wnfc 2550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-nf 1662  df-nfc 2552
This theorem is referenced by:  nfcvd  2564  nfeq1  2576  nfel1  2577  nfeq2  2578  nfel2  2579  nfcvf  2586  r2alOLD  2738  nfra2  2746  r2exOLD  2885  r19.12  2887  ralcom  2922  rexcom  2923  raleq  2958  rexeq  2959  reueq1  2960  rmoeq1  2961  cbvral  2986  cbvrex  2987  rabeq  3009  cbvrabv  3015  vtocl2g  3079  vtoclga  3081  vtocl2ga  3083  vtocl3ga  3085  spcimdv  3099  spcgv  3102  spcegv  3103  rspct  3111  rspc  3112  rspce  3113  rspc2  3126  elabgt  3150  elabf  3152  elabg  3154  elab3g  3159  elrab  3164  2rmorex  3212  nfsbc1v  3255  elrabsf  3274  sbcralt  3308  sbcralg  3310  sbcrex  3311  sbcreu  3312  cbvcsbv  3337  csbconstg  3344  nfcsb1v  3347  csbie  3357  cbvralcsf  3363  cbvreucsf  3365  cbvrabcsf  3366  cbvralv2  3367  cbvrexv2  3368  n0f  3706  n0  3707  csbnestg  3753  raaan  3843  nfpw  3929  nfop  4139  rabasiun  4239  cbviunv  4274  cbviinv  4275  ssiun2s  4279  iunab  4281  ssiinf  4284  ssiin  4285  iinab  4296  cbvdisjv  4341  disjors  4345  disji2  4346  invdisjrab  4349  disjprg  4355  disjxiun  4356  disjxun  4357  cbvmptv  4452  triun  4467  zfrep3cl  4479  csbexg  4494  eusvnf  4555  reusv2lem4  4564  reusv2  4566  rabxfrd  4578  moop2  4651  euotd  4657  opelopabgf  4676  opelopabf  4681  nfpo  4715  nfso  4716  pofun  4726  nffr  4763  nfse  4764  opeliunxp  4841  nfrel  4875  ralxpf  4936  nfco  4955  nfcnv  4968  dfdmf  4983  dfrnf  5028  nfdm  5031  nfres  5062  wfisg  5370  dffun6f  5551  dffun6  5552  nffun  5559  nffv  5825  nffvmpt1  5826  dffn5f  5873  funfv2f  5887  fvmpt2f  5902  fvmpts  5904  fvmpt2i  5909  fvmptss  5911  fvmptex  5913  fvmptdv  5915  fvmptnf  5920  fvmptn  5921  elfvmptrab1  5923  fvopab5  5926  eqfnfv2f  5932  ralrnmpt  5983  f1ompt  5996  ffnfvf  6002  fmptco  6008  fmptcof  6009  fmptcos  6010  funiunfvf  6106  dff13f  6112  f1mpt  6114  fliftfuns  6159  nfiso  6167  csbriota  6216  riota2  6226  riotaxfrd  6234  oprabv  6290  mpt2eq123  6301  cbvmpt2x  6320  cbvmpt2  6321  cbvmpt2v  6322  ovmpt2s  6371  ov2gf  6372  ovmpt2dxf  6373  ovmpt2dx  6374  ovmpt2dv  6380  ovmpt2dv2  6381  ov3  6384  elovmpt2rab  6466  elovmpt2rab1  6467  ovmpt3rab1  6476  ovmpt3rabdm  6477  elovmpt3rab1  6478  nfof  6487  nfofr  6488  offval2f  6494  offval2  6499  ofrfval2  6500  ofmpteq  6501  onminesb  6576  onminsb  6577  tfis  6632  tfisi  6636  zfrep6  6712  abrexex2g  6721  abrexex2  6725  dfopab2  6798  dfoprab3s  6799  mpt2mptsx  6807  dmmpt2ssx  6809  fmpt2x  6810  fnmpt2ovd  6822  offval22  6823  ovmptss  6825  fmpt2co  6827  dfmpt2  6834  mpt2xopoveq  6913  mpt2xopovel  6914  nftpos  6956  tposoprab  6957  mpt2curryd  6964  mpt2curryvald  6965  fvmpt2curryd  6966  nfwrecs  6978  nfrecs  7041  nfrdg  7080  rdgsucmpt2  7096  rdgsucmpt  7097  frsucmpt  7103  frsucmptn  7104  frsucmpt2  7105  oawordeulem  7203  nnawordex  7286  qliftfuns  7398  cbvixpv  7488  nfixp  7489  nfixp1  7490  ixpf  7492  mptelixpg  7507  dom2lem  7556  xpcomco  7608  xpf1o  7680  mapxpen  7684  ac6sfi  7761  iunfi  7808  indexfi  7828  dffi3  7891  nfoi  7975  ixpiunwdom  8052  cantnflem1  8139  cnfcomlem  8149  r1val1  8202  rankidb  8216  rankval4  8283  scottex  8301  scottexs  8303  scott0s  8304  cp  8307  tskwe  8329  cardmin2  8377  fseqenlem1  8399  dfac8clem  8407  cardaleph  8464  hsmexlem2  8801  axcc2  8811  ac6num  8853  ac6c4  8855  axdclem  8893  iundom2g  8909  uniimadomf  8914  cardmin  8933  pwfseqlem2  9028  pwfseqlem4a  9030  pwfseqlem4  9031  inar1  9144  lble  10502  nnwof  11169  nnwos  11170  fzrevral  11823  rabssnn0fi  12141  nfseq  12166  seqof2  12214  hashrabsn1  12496  nfwrd  12636  relexpsucnnr  13025  rlim2  13496  ello1mpt  13521  rlimcld2  13578  o1compt  13587  nfsum1  13692  nfsum  13693  sumeq2ii  13695  cbvsumv  13698  cbvsumi  13699  sumfc  13711  summolem2a  13717  zsum  13720  sumss  13726  sumss2  13728  fsumcvg2  13729  fsumzcl2  13740  fsumadd  13741  sumsn  13743  sumsns  13747  fsummsnunz  13751  fsumsplitsnun  13752  fsum2dlem  13767  fsumcom2  13771  fsumshftm  13778  fsummulc2  13781  fsum00  13794  fsumrelem  13803  fsumrlim  13807  fsumo1  13808  o1fsum  13809  fsumiun  13817  prodeq1  13899  nfcprod1  13900  nfcprod  13901  cbvprod  13905  cbvprodv  13906  cbvprodi  13907  prodmolem2a  13924  zprod  13927  fprod  13931  fprodntriv  13932  prodfc  13935  prodss  13937  fprodcllemf  13948  fprodmul  13950  fproddiv  13951  prodsn  13952  prodsnf  13954  fprodm1s  13960  fprodp1s  13961  prodsns  13962  fprodn0  13969  fprod2dlem  13970  fprodcom2  13974  fproddivf  13977  fprodsplitf  13978  fprodsplit1f  13980  fprodle  13986  fprodefsum  14085  prmind2  14571  coprmprod  14614  coprmproddvdslem  14615  pcmpt  14773  pcmptdvds  14775  prdsbas3  15315  prdsdsval2  15318  mreiincl  15438  invfuc  15815  yonedalem4b  16097  gsumconstf  17504  gsumsnd  17521  gsumsn  17523  gsumunsnd  17526  gsummpt1n0  17533  gsum2d2lem  17541  gsum2d2  17542  gsumcom2  17543  prdsgsum  17546  dprd2d2  17613  gsumdixp  17773  lss1d  18122  psrass1lem  18537  evlslem4  18667  mpfrcl  18677  coe1fzgsumdlem  18831  gsummoncoe1  18834  gsumply1eq  18835  evl1gsumdlem  18880  mdetralt2  19569  mdetunilem2  19573  madugsum  19603  gsummatr01lem4  19618  cayleyhamilton1  19851  neiptopnei  20083  fiuncmp  20354  iuncon  20378  2ndcdisj  20406  dissnlocfin  20479  elptr2  20524  ptbasfi  20531  ptunimpt  20545  ptcldmpt  20564  ptclsg  20565  ptcnplem  20571  ptcnp  20572  cnmpt11  20613  cnmpt1t  20615  cnmpt21  20621  cnmpt2t  20623  cnmptcom  20628  cnmptk2  20636  cnmpt2k  20638  imasnopn  20640  imasncld  20641  imasncls  20642  xkocnv  20764  elmptrab  20777  flfcnp2  20957  ptcmpg  21007  fmucnd  21242  prdsdsf  21317  prdsxmet  21319  cfilucfil  21509  blval2  21512  restmetu  21520  fsumcn  21837  fsum2cn  21838  ovolfiniun  22389  ovoliunlem3  22392  ovoliun  22393  ovoliun2  22394  ovoliunnul  22395  finiunmbl  22432  volfiniun  22435  iundisj  22436  iundisj2  22437  iunmbl  22441  voliun  22442  iunmbl2  22445  mbfpos  22542  mbfposr  22543  mbfposb  22544  mbfsup  22555  mbfinf  22556  mbfinfOLD  22557  mbflim  22561  i1fposd  22600  itg1climres  22607  itg2splitlem  22641  itg2split  22642  itg2cnlem1  22654  isibl2  22659  itgeq1  22665  nfitg1  22666  nfitg  22667  cbvitg  22668  cbvitgv  22669  itgmpt  22675  itgss3  22707  itgfsum  22719  itgabs  22727  itggt0  22734  itgcn  22735  cbvditgv  22745  limcmpt  22773  limciun  22784  dvmptfsum  22862  dvlipcn  22881  lhop2  22902  dvfsumle  22908  dvfsumabs  22910  dvfsumlem1  22913  dvfsumlem2  22914  dvfsumlem4  22916  dvfsumrlim  22918  dvfsum2  22921  itgparts  22934  itgsubstlem  22935  itgsubst  22936  elplyd  23091  coeeq2  23131  dgrle  23132  ulmss  23287  itgulm2  23299  leibpi  23803  rlimcnp  23826  rlimcnp2  23827  o1cxp  23835  lgamgulmlem2  23890  lgamgulmlem6  23894  lgamgulm2  23896  fsumdvdscom  24049  fsumdvdsmul  24059  fsumvma  24076  lgseisenlem2  24213  dchrisumlema  24261  dchrisumlem2  24263  dchrisumlem3  24264  nbgraopALT  25087  cnlnadjlem5  27659  chirred  27983  vtocl2d  28044  ralcom4f  28045  rexcom4f  28046  rmo4fOLD  28067  rabtru  28071  iunin1f  28110  iunxsngf  28111  iunxdif3  28114  disji2f  28126  disjorsf  28129  disjif2  28130  disjabrex  28131  disjabrexf  28132  iundisjf  28138  iundisj2f  28139  disjunsn  28143  dfrel4  28147  ac6sf2  28165  dfimafnf  28172  suppss2fOLD  28176  suppss2f  28177  fimarab  28183  fmptdF  28194  resmptf  28196  feqmptdf  28197  fmptcof2  28198  fcomptf  28199  acunirnmpt2  28201  acunirnmpt2f  28202  aciunf1lem  28203  aciunf1  28204  ofpreima  28207  funcnvmptOLD  28209  funcnvmpt  28210  funcnv5mpt  28211  funcnv4mpt  28212  f1od2  28252  fpwrelmap  28261  fpwrelmapffs  28262  xrofsup  28296  iundisjfi  28315  iundisj2fi  28316  iundisjcnt  28317  iundisj2cnt  28318  nnindf  28326  gsummpt2co  28487  gsumvsca1  28490  gsumvsca2  28491  mdetpmtr1  28594  ordtconlem1  28675  qqhval2  28731  esumcl  28796  nfesum1  28806  nfesum2  28807  cbvesumv  28809  esumid  28810  esumgsum  28811  esumval  28812  esumel  28813  esumnul  28814  esumc  28817  esumrnmpt  28818  esumsplit  28819  esummono  28820  esumpad  28821  esumpad2  28822  esumadd  28823  esumle  28824  gsumesum  28825  esumlub  28826  esumaddf  28827  esumsnf  28830  esumsn  28831  esumpr  28832  esumrnmpt2  28834  esumfzf  28835  esumfsup  28836  esumss  28838  esumpinfval  28839  esumpfinvalf  28842  esumpinfsum  28843  esumpcvgval  28844  esumpmono  28845  esumcocn  28846  esummulc1  28847  esummulc2  28848  esumdivc  28849  esumcvg  28852  esumsup  28855  esumgect  28856  esum2dlem  28858  esum2d  28859  esumiun  28860  sigaclcu2  28887  ldsysgenld  28927  sigapildsys  28929  ldgenpisyslem1  28930  fiunelros  28941  measvunilem  28979  measvunilem0  28980  measvuni  28981  measiuns  28984  measiun  28985  meascnbl  28986  voliune  28997  volfiniune  28998  volmeas  28999  ddemeas  29004  imambfm  29029  omscl  29064  omsclOLD  29068  oms0  29070  omsmon  29071  omssubadd  29073  oms0OLD  29074  omsmonOLD  29075  omssubaddOLD  29077  carsgclctunlem1  29094  carsggect  29095  carsgclctunlem2  29096  omsmeas  29100  omsmeasOLD  29101  sibfof  29118  eulerpartlemn  29159  bnj23  29469  bnj1366  29586  bnj1400  29592  bnj1534  29609  bnj1542  29613  bnj607  29672  bnj873  29680  bnj958  29696  bnj1000  29697  bnj981  29706  bnj1014  29716  bnj1123  29740  bnj1204  29766  bnj1388  29787  bnj1398  29788  bnj1408  29790  bnj1445  29798  bnj1446  29799  bnj1447  29800  bnj1448  29801  bnj1449  29802  bnj1466  29807  bnj1467  29808  bnj1463  29809  bnj1312  29812  bnj1498  29815  bnj1519  29819  bnj1520  29820  bnj1525  29823  bnj1529  29824  cvmcov  29931  setinds  30368  dfon2lem3  30375  tfisg  30401  trpredlem1  30412  trpredtr  30415  trpredmintr  30416  trpred0  30421  trpredrec  30423  frinsg  30427  nfwlim  30449  sltval2  30487  nobndlem5  30527  finminlem  30916  bj-rabtrALT  31440  topdifinfindis  31650  topdifinffinlem  31651  isbasisrelowllem1  31659  isbasisrelowllem2  31660  iooelexlt  31666  relowlssretop  31667  finxpreclem2  31683  finxpreclem6  31689  phpreu  31830  finixpnum  31831  ptrest  31840  poimirlem16  31857  poimirlem19  31860  poimirlem23  31864  poimirlem24  31865  poimirlem25  31866  poimirlem26  31867  poimirlem27  31868  poimirlem28  31869  mbfposadd  31889  dvtanlemOLD  31892  itgabsnc  31912  itggt0cn  31915  ftc1cnnclem  31916  ftc1anclem5  31922  ftc2nc  31927  indexa  31961  indexdom  31962  filbcmb  31968  sdclem2  31972  sdclem1  31973  fdc1  31976  totbndbnd  32022  heibor1  32043  scottexf  32312  scott0f  32313  ac6s6f  32317  fsumshftd  32429  fsumshftdOLD  32430  riotasvd  32434  riotasv2d  32435  riotasv2s  32436  riotaocN  32681  cdleme26ee  33833  cdleme31sn1  33854  cdleme31se2  33856  cdlemefrs29bpre0  33869  cdlemefs32sn1aw  33887  cdleme43fsv1snlem  33893  cdleme41sn3a  33906  cdleme32d  33917  cdleme32f  33919  cdleme40m  33940  cdleme40n  33941  cdleme42b  33951  ltrniotaval  34054  cdlemksv2  34320  cdlemkuv2  34340  cdlemk36  34386  cdlemk38  34388  cdlemkid  34409  cdlemk19x  34416  cdlemk11t  34419  dihglblem5  34772  hlhilset  35411  elrfirn2  35444  mzpsubst  35496  eq0rabdioph  35525  sbcrexgOLD  35534  sbccomieg  35542  rexrabdioph  35543  rexfrabdioph  35544  rabdiophlem2  35551  elnn0rabdioph  35552  dvdsrabdioph  35559  rabrenfdioph  35563  monotoddzz  35698  oddcomabszz  35699  setindtrs  35787  wdom2d2  35797  aomclem6  35824  aomclem8  35826  areaquad  36008  ss2iundv  36159  cbviuneq12dv  36161  binomcxplemdvbinom  36609  binomcxplemdvsum  36611  binomcxplemnotnn0  36612  compab  36701  iunconlem2  37242  evth2f  37246  elunif  37247  fvelrnbf  37249  rfcnpre1  37250  fsumcnf  37252  sumsnd  37257  evthf  37258  refsumcn  37261  rfcnpre2  37262  rfcnpre3  37264  rfcnpre4  37265  rfcnnnub  37267  refsum2cnlem1  37268  refsum2cn  37269  uzwo4  37302  iunxsngf2  37312  fiiuncl  37316  suprnmpt  37336  dffo3f  37348  elrnmptf  37352  disjf1  37355  wessf1ornlem  37357  disjrnmpt2  37361  disjf1o  37364  fompt  37365  disjinfi  37366  ssfiunibd  37418  supxrgere  37447  iuneqfzuzlem  37448  supxrgelem  37451  supxrge  37452  fsumclf  37523  fsumsplitf  37524  fsummulc1f  37525  sumsnf  37526  fsumsplit1  37529  fsumf1of  37531  fsumiunss  37532  fsumreclf  37533  fsumlessf  37534  fmul01  37535  fmuldfeqlem1  37537  fmuldfeq  37538  fmul01lt1lem1  37539  fmul01lt1lem2  37540  fmul01lt1  37541  cncfmptss  37542  mulc1cncfg  37544  infrglbOLD  37546  expcnfg  37548  fprodexp  37551  fprodabs2  37552  mccllem  37554  mccl  37555  climmulf  37559  climexp  37560  climsuse  37564  climrecf  37565  climinff  37567  climinffOLD  37568  climaddf  37572  mullimc  37573  constlimc  37581  idlimc  37583  limcperiod  37585  sumnnodd  37587  neglimc  37605  addlimc  37606  0ellimcdiv  37607  cncfshift  37628  icccncfext  37642  cncficcgt0  37643  cncfiooicclem1  37648  fprodcncf  37656  dvcosre  37658  dvmptmulf  37689  dvnmptdivc  37690  dvnmul  37695  dvmptfprodlem  37696  dvmptfprod  37697  dvnprodlem1  37698  dvnprodlem2  37699  itgsin0pilem1  37703  ibliccsinexp  37704  itgsinexplem1  37707  itgsinexp  37708  iblsplitf  37724  itgsubsticclem  37729  stoweidlem3  37740  stoweidlem14  37751  stoweidlem16  37753  stoweidlem18  37755  stoweidlem21  37758  stoweidlem23  37760  stoweidlem26  37763  stoweidlem27  37764  stoweidlem28  37765  stoweidlem29  37766  stoweidlem29OLD  37767  stoweidlem31  37769  stoweidlem34  37772  stoweidlem35  37773  stoweidlem36  37774  stoweidlem41  37779  stoweidlem42  37780  stoweidlem43  37781  stoweidlem46  37784  stoweidlem47  37785  stoweidlem48  37786  stoweidlem51  37789  stoweidlem52  37790  stoweidlem53  37791  stoweidlem54  37792  stoweidlem55  37793  stoweidlem56  37794  stoweidlem57  37795  stoweidlem58  37796  stoweidlem59  37797  stoweidlem60  37798  stoweidlem62  37800  stoweidlem62OLD  37801  stowei  37803  wallispilem5  37808  stirlinglem4  37816  stirlinglem5  37817  stirlinglem11  37823  stirlinglem12  37824  stirlinglem13  37825  stirlinglem14  37826  stirlinglem15  37827  stirling  37828  fourierdlem20  37866  fourierdlem31  37877  fourierdlem31OLD  37878  fourierdlem48  37895  fourierdlem51  37898  fourierdlem68  37915  fourierdlem73  37920  fourierdlem79  37926  fourierdlem80  37927  fourierdlem86  37933  fourierdlem89  37936  fourierdlem91  37938  fourierdlem103  37950  fourierdlem104  37951  fourierdlem112  37959  fourierdlem115  37962  fourierd  37963  fourierclimd  37964  etransclem2  37978  etransclem24  38000  etransclem25  38001  etransclem26  38002  etransclem28  38004  etransclem32  38008  etransclem35  38011  etransclem37  38013  etransclem44  38020  etransclem46  38022  etransclem48OLD  38024  etransclem48  38025  sge00  38063  sge0revalmpt  38065  sge0f1o  38069  sge0fsummpt  38077  sge0pnffigt  38083  sge0lefi  38085  sge0ltfirp  38087  sge0resplit  38093  sge0lempt  38097  sge0iunmptlemfi  38100  sge0iunmptlemre  38102  sge0fodjrnlem  38103  sge0iunmpt  38105  sge0ltfirpmpt2  38113  sge0isummpt2  38119  sge0xaddlem2  38121  sge0xadd  38122  sge0fsummptf  38123  sge0gtfsumgt  38130  iundjiun  38143  meadjiun  38149  omeiunle  38183  omeiunltfirp  38185  carageniuncllem1  38187  caratheodorylem1  38192  caratheodorylem2  38193  hoicvrrex  38219  ovnlerp  38225  ovncvrrp  38227  ovn0lem  38228  hoidmvval0  38250  hoidmvlelem1  38258  hoidmvlelem3  38260  ovnhoilem1  38264  cbvral2  38401  cbvrex2  38402  raaan2  38404  2reurex  38410  2reu3  38417  2reu7  38420  2reu8  38421  eu2ndop1stv  38431  nfafv  38445  iunopeqop  38807  fsummsndifre  38859  fsumsplitsndif  38860  fsummmodsndifre  38861  fsummmodsnunz  38862  gropd  38901  grstructd  38902  opeliun2xp  39701  dmmpt2ssx2  39705  ovmpt2rdxf  39707  ovmpt2rdx  39708  aacllem  40127
  Copyright terms: Public domain W3C validator