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

Theorem nfcv 2540
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 1626 . 2  |-  F/ x  y  e.  A
21nfci 2530 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   F/_wnfc 2527
This theorem is referenced by:  nfcvd  2541  nfel  2548  nfeq1  2549  nfel1  2550  nfeq2  2551  nfel2  2552  nfcvf  2562  r2al  2703  r2ex  2704  nfra2  2720  r19.12  2779  ralcom  2828  rexcom  2829  raleq  2864  rexeq  2865  reueq1  2866  rmoeq1  2867  cbvral  2888  cbvrex  2889  rabeq  2910  cbvrabv  2915  vtoclg  2971  vtocl2g  2975  vtoclga  2977  vtocl2ga  2979  vtocl3ga  2981  spcimdv  2993  spcgv  2996  spcegv  2997  rspct  3005  rspc  3006  rspce  3007  rspc2  3017  ceqsexg  3027  elabgt  3039  elabf  3041  elabg  3043  elab3g  3048  elrab  3052  mob  3076  2rmorex  3098  nfsbc1v  3140  elrabsf  3159  sbcralt  3193  sbcralg  3195  sbcrexg  3196  sbcreug  3197  cbvcsbv  3216  csbexg  3221  csbconstg  3225  nfcsb1v  3243  csbnestg  3261  cbvralcsf  3271  cbvreucsf  3273  cbvrabcsf  3274  cbvralv2  3275  cbvrexv2  3276  n0f  3596  n0  3597  raaan  3695  nfpw  3770  nfop  3960  cbviunv  4090  cbviinv  4091  ssiun2s  4095  iunab  4097  ssiinf  4100  ssiin  4101  iinab  4112  cbvdisjv  4153  disjors  4158  disji2  4159  disjprg  4168  disjxiun  4169  disjxun  4170  cbvmptv  4260  triun  4275  zfrep3cl  4287  moop2  4411  euotd  4417  opelopabf  4439  nfpo  4468  nfso  4469  pofun  4479  nffr  4516  nfse  4517  eusvnf  4677  reusv2lem4  4686  reusv2  4688  reusv6OLD  4693  rabxfrd  4703  onminesb  4737  onminsb  4738  tfis  4793  tfisi  4797  opeliunxp  4888  nfrel  4921  opeliunxp2  4972  ralxpf  4978  nfco  4997  nfcnv  5010  dfdmf  5023  dfrnf  5067  nfdm  5070  nfres  5107  dffun6f  5427  dffun6  5428  nffun  5435  nffv  5694  nffvmpt1  5695  dffn5f  5740  funfv2f  5751  fvmpts  5766  fvmpt2i  5770  fvmptss  5772  fvmptex  5774  fvmptdv  5776  fvmptnf  5781  fvmptn  5782  eqfnfv2f  5790  ralrnmpt  5837  f1ompt  5850  ffnfvf  5854  fmptco  5860  fmptcof  5861  fmptcos  5862  zfrep6  5927  abrexex2g  5947  funiunfvf  5955  abrexex2  5960  dff13f  5965  f1mpt  5966  fliftfuns  5995  nfiso  6003  mpt2eq123  6092  cbvmpt2x  6109  cbvmpt2  6110  cbvmpt2v  6111  ovmpt2s  6156  ov2gf  6157  ovmpt2dxf  6158  ovmpt2dx  6159  ovmpt2dv  6165  ovmpt2dv2  6166  ov3  6169  nfof  6269  nfofr  6270  offval2  6281  ofrfval2  6282  dfopab2  6360  dfoprab3s  6361  mpt2mptsx  6373  dmmpt2ssx  6375  fmpt2x  6376  ovmptss  6387  fmpt2co  6389  dfmpt2  6396  mpt2xopoveq  6429  mpt2xopovel  6430  nftpos  6473  tposoprab  6474  fvopab5  6493  nfriota1  6516  csbriotag  6521  riota2  6531  riotaxfrd  6540  riotasvd  6551  riotasvdOLD  6552  riotasv2d  6553  riotasv2dOLD  6554  riotasv2s  6555  riotasv3dOLD  6558  nfrecs  6594  nfrdg  6631  rdgsucmpt2  6647  rdgsucmpt  6648  frsucmpt  6654  frsucmptn  6655  frsucmpt2  6656  oawordeulem  6756  nnawordex  6839  eqerlem  6896  qliftfuns  6950  cbvixpv  7039  nfixp  7040  nfixp1  7041  ixpf  7043  mptelixpg  7058  dom2lem  7106  xpcomco  7157  xpf1o  7228  mapxpen  7232  ac6sfi  7310  iunfi  7353  indexfi  7372  dffi3  7394  nfoi  7439  ixpiunwdom  7515  cnfcomlem  7612  r1val1  7668  rankidb  7682  rankval4  7749  scottex  7765  scottexs  7767  scott0s  7768  cp  7771  tskwe  7793  cardmin2  7841  fseqenlem1  7861  dfac8clem  7869  cardaleph  7926  hsmexlem2  8263  axcc2  8273  ac6num  8315  ac6c4  8317  axdclem  8355  iundom2g  8371  uniimadomf  8376  cardmin  8395  pwfseqlem2  8490  pwfseqlem4a  8492  pwfseqlem4  8493  inar1  8606  lble  9916  nnwof  10499  nnwos  10500  fzrevral  11086  nfseq  11288  seqof2  11336  nfwrd  11695  rlim2  12245  ello1mpt  12270  rlimcld2  12327  o1compt  12336  sumeq1  12438  nfsum1  12439  nfsum  12440  sumeq2w  12441  cbvsum  12444  cbvsumv  12445  cbvsumi  12446  sumfc  12458  summolem2a  12464  zsum  12467  fsum  12469  sumss  12473  sumss2  12475  fsumcvg2  12476  fsumadd  12487  sumsn  12489  sumsns  12491  fsum2dlem  12509  fsumcnv  12512  fsumcom2  12513  fsumshftm  12519  fsum0diag2  12521  fsummulc2  12522  fsum00  12532  fsumrelem  12541  fsumrlim  12545  fsumo1  12546  o1fsum  12547  fsumiun  12555  ruclem1  12785  prmind2  13045  pcmpt  13216  pcmptdvds  13218  prdsbas3  13658  prdsdsval2  13661  mreiincl  13776  invfuc  14126  yonedalem4b  14328  odval  15127  gsum2d2lem  15502  gsum2d2  15503  gsumcom2  15504  prdsgsum  15507  dprd2d2  15557  gsumdixp  15670  lss1d  15994  psrass1lem  16397  evlslem4  16519  neiptopnei  17151  fiuncmp  17421  iuncon  17444  2ndcdisj  17472  elptr2  17559  ptbasfi  17566  ptunimpt  17580  ptcldmpt  17599  ptclsg  17600  ptcnplem  17606  ptcnp  17607  cnmpt11  17648  cnmpt1t  17650  cnmpt21  17656  cnmpt2t  17658  cnmptcom  17663  cnmptk2  17671  cnmpt2k  17673  imasnopn  17675  imasncld  17676  imasncls  17677  xkocnv  17799  elmptrab  17812  flfcnp2  17992  ptcmpg  18041  cnextfvval  18049  fmucnd  18275  prdsdsf  18350  prdsxmet  18352  cfilucfilOLD  18552  cfilucfil  18553  blval2  18558  restmetu  18570  fsumcn  18853  fsum2cn  18854  ovolfiniun  19350  ovoliunlem3  19353  ovoliun  19354  ovoliun2  19355  ovoliunnul  19356  finiunmbl  19391  volfiniun  19394  iundisj  19395  iundisj2  19396  iunmbl  19400  voliun  19401  iunmbl2  19404  mbfpos  19496  mbfposr  19497  mbfposb  19498  mbfsup  19509  mbfinf  19510  mbflim  19513  i1fposd  19552  itg1climres  19559  itg2splitlem  19593  itg2split  19594  itg2cnlem1  19606  isibl  19610  isibl2  19611  dfitg  19614  itgeq1  19617  nfitg1  19618  nfitg  19619  cbvitg  19620  cbvitgv  19621  itgmpt  19627  itgss3  19659  itgfsum  19671  itgabs  19679  itggt0  19686  itgcn  19687  cbvditgv  19695  limcmpt  19723  limciun  19734  dvmptfsum  19812  dvlipcn  19831  lhop2  19852  dvfsumle  19858  dvfsumabs  19860  dvfsumlem1  19863  dvfsumlem2  19864  dvfsumlem4  19866  dvfsumrlim  19868  dvfsum2  19871  itgparts  19884  itgsubstlem  19885  itgsubst  19886  mpfrcl  19892  elplyd  20074  coeeq2  20114  dgrle  20115  ulmss  20266  itgulm2  20278  leibpi  20735  rlimcnp  20757  rlimcnp2  20758  o1cxp  20766  fsumdvdscom  20923  fsumdvdsmul  20933  fsumvma  20950  lgseisenlem2  21087  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  cnlnadjlem5  23527  chirred  23851  ralcom4f  23918  rexcom4f  23919  rmo4fOLD  23936  disji2f  23972  disjorsf  23975  disjif2  23976  disjabrex  23977  disjabrexf  23978  disjxpin  23981  iundisjf  23982  iundisj2f  23983  dfrel4  23987  dfimafnf  23996  suppss2f  24002  fmptdF  24022  resmptf  24024  fvmpt2f  24025  feqmptdf  24028  fmptcof2  24029  fcomptf  24030  offval2f  24033  ofpreima  24034  funcnvmptOLD  24035  funcnvmpt  24036  funcnv5mpt  24037  funcnv4mpt  24038  xrofsup  24079  iundisjfi  24105  iundisj2fi  24106  iundisjcnt  24107  iundisj2cnt  24108  gsumconstf  24175  xrge0tmd  24285  qqhval2  24319  esumcl  24380  nfesum1  24390  cbvesumv  24392  esumid  24393  esumval  24394  esumel  24395  esumnul  24396  esumsplit  24400  esumadd  24401  esumle  24402  esummono  24403  gsumesum  24404  esumlub  24405  esumaddf  24406  esumpr  24410  esumfzf  24412  esumfsup  24413  esumss  24415  esumpinfval  24416  esumpfinvalf  24419  esumpinfsum  24420  esumpcvgval  24421  esumpmono  24422  esumcocn  24423  esummulc1  24424  esummulc2  24425  esumdivc  24426  esumcvg  24429  sigaclcu2  24456  measvunilem  24519  measvunilem0  24520  measvuni  24521  measiuns  24524  measiun  24525  meascnbl  24526  voliune  24538  volfiniune  24539  volmeas  24540  imambfm  24565  sibfof  24607  lgamgulmlem2  24767  lgamgulmlem6  24771  lgamgulm2  24773  cvmcov  24903  relexpsucr  25083  prodeq1  25188  nfcprod1  25189  nfcprod  25190  prodeq2w  25191  cbvprod  25194  cbvprodv  25195  cbvprodi  25196  prodmolem2a  25213  zprod  25216  fprod  25220  fprodntriv  25221  prodfc  25224  prodss  25226  fprodmul  25237  fproddiv  25238  prodsn  25239  fprodm1s  25246  fprodp1s  25247  prodsns  25248  fprodefsum  25251  fprodn0  25256  fprod2dlem  25257  fprodcnv  25260  fprodcom2  25261  setinds  25348  dfon2lem3  25355  tfisg  25418  wfisg  25423  trpredlem1  25444  trpredtr  25447  trpredmintr  25448  trpred0  25453  trpredrec  25455  frinsg  25459  sltval2  25524  nobndlem5  25564  bpolyval  25999  mbfposadd  26153  itgabsnc  26173  itggt0cn  26176  ftc1cnnclem  26177  finminlem  26211  indexa  26325  indexdom  26326  filbcmb  26332  sdclem2  26336  sdclem1  26337  fdc1  26340  totbndbnd  26388  heibor1  26409  elrfirn2  26640  ofmpteq  26666  mzpsubst  26695  eq0rabdioph  26725  sbccomieg  26739  rexrabdioph  26744  rexfrabdioph  26745  rabdiophlem2  26752  elnn0rabdioph  26753  dvdsrabdioph  26760  rabrenfdioph  26765  fphpd  26767  monotuz  26894  monotoddzz  26896  oddcomabszz  26897  setindtrs  26986  wdom2d2  26996  fnwe2val  27014  fnwe2lem1  27015  aomclem6  27024  aomclem8  27027  mamufval  27311  compab  27511  evth2f  27553  elunif  27554  fvelrnbf  27556  rfcnpre1  27557  fsumcnf  27559  sumsnd  27564  evthf  27565  refsumcn  27568  rfcnpre2  27569  rfcnpre3  27571  rfcnpre4  27572  rfcnnnub  27574  refsum2cnlem1  27575  refsum2cn  27576  fmul01  27577  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  fmul01lt1  27583  cncfmptss  27584  mulc1cncfg  27588  infrglb  27589  expcnfg  27593  climmulf  27597  climexp  27598  climsuse  27601  climrecf  27602  climinff  27604  dvcosre  27608  itgsin0pilem1  27611  ibliccsinexp  27612  itgsinexplem1  27615  itgsinexp  27616  stoweidlem3  27619  stoweidlem14  27630  stoweidlem16  27632  stoweidlem18  27634  stoweidlem21  27637  stoweidlem23  27639  stoweidlem26  27642  stoweidlem27  27643  stoweidlem28  27644  stoweidlem29  27645  stoweidlem31  27647  stoweidlem34  27650  stoweidlem35  27651  stoweidlem36  27652  stoweidlem41  27657  stoweidlem42  27658  stoweidlem43  27659  stoweidlem46  27662  stoweidlem47  27663  stoweidlem48  27664  stoweidlem51  27667  stoweidlem52  27668  stoweidlem53  27669  stoweidlem54  27670  stoweidlem55  27671  stoweidlem56  27672  stoweidlem57  27673  stoweidlem58  27674  stoweidlem59  27675  stoweidlem60  27676  stoweidlem62  27678  stowei  27680  wallispilem5  27685  stirlinglem4  27693  stirlinglem5  27694  stirlinglem11  27700  stirlinglem12  27701  stirlinglem13  27702  stirlinglem14  27703  stirlinglem15  27704  stirling  27705  cbvral2  27817  cbvrex2  27818  raaan2  27820  2reurex  27826  2reu3  27833  2reu7  27836  2reu8  27837  eu2ndop1stv  27847  nfafv  27867  bnj23  28789  bnj1366  28907  bnj1400  28913  bnj1534  28930  bnj1542  28934  bnj607  28993  bnj873  29001  bnj958  29017  bnj1000  29018  bnj981  29027  bnj1014  29037  bnj1123  29061  bnj1204  29087  bnj1388  29108  bnj1398  29109  bnj1408  29111  bnj1445  29119  bnj1446  29120  bnj1447  29121  bnj1448  29122  bnj1449  29123  bnj1466  29128  bnj1467  29129  bnj1463  29130  bnj1312  29133  bnj1498  29136  bnj1519  29140  bnj1520  29141  bnj1525  29144  bnj1529  29145  riotaocN  29692  cdleme26ee  30842  cdleme31sn1  30863  cdleme31se2  30865  cdlemefrs29bpre0  30878  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme41sn3a  30915  cdleme32d  30926  cdleme32f  30928  cdleme40m  30949  cdleme40n  30950  cdleme42b  30960  ltrniotaval  31063  cdlemksv2  31329  cdlemkuv2  31349  cdlemk36  31395  cdlemk38  31397  cdlemkid  31418  cdlemk19x  31425  cdlemk11t  31428  dihglblem5  31781  hlhilset  32420
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-nf 1551  df-nfc 2529
  Copyright terms: Public domain W3C validator