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

Theorem nfcv 2616
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 1712 . 2  |-  F/ x  y  e.  A
21nfci 2605 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823   F/_wnfc 2602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-5 1709
This theorem depends on definitions:  df-bi 185  df-nf 1622  df-nfc 2604
This theorem is referenced by:  nfcvd  2617  nfelOLD  2630  nfeq1  2631  nfel1  2632  nfeq2  2633  nfel2  2634  nfcvf  2641  r2alOLD  2833  nfra2  2841  r2exOLD  2978  r19.12  2980  ralcom  3015  rexcom  3016  raleq  3051  rexeq  3052  reueq1  3053  rmoeq1  3054  cbvral  3077  cbvrex  3078  rabeq  3100  cbvrabv  3105  vtocl2g  3168  vtoclga  3170  vtocl2ga  3172  vtocl3ga  3174  spcimdv  3188  spcgv  3191  spcegv  3192  rspct  3200  rspc  3201  rspce  3202  rspc2  3215  elabgt  3240  elabf  3242  elabg  3244  elab3g  3249  elrab  3254  2rmorex  3301  nfsbc1v  3344  elrabsf  3363  sbcralt  3397  sbcralg  3399  sbcrex  3400  sbcreu  3401  cbvcsbv  3426  csbconstg  3433  nfcsb1v  3436  csbie  3446  cbvralcsf  3452  cbvreucsf  3454  cbvrabcsf  3455  cbvralv2  3456  cbvrexv2  3457  n0f  3792  n0  3793  csbnestg  3837  raaan  3925  nfpw  4011  nfop  4219  rabasiun  4319  cbviunv  4354  cbviinv  4355  ssiun2s  4359  iunab  4361  ssiinf  4364  ssiin  4365  iinab  4376  cbvdisjv  4421  disjors  4425  disji2  4426  invdisjrab  4429  disjprg  4435  disjxiun  4436  disjxun  4437  cbvmptv  4530  triun  4545  zfrep3cl  4557  csbexg  4571  eusvnf  4632  reusv2lem4  4641  reusv2  4643  reusv6OLD  4648  rabxfrd  4658  moop2  4731  euotd  4737  opelopabgf  4756  opelopabf  4761  nfpo  4794  nfso  4795  pofun  4805  nffr  4842  nfse  4843  opeliunxp  5040  nfrel  5076  ralxpf  5138  nfco  5157  nfcnv  5170  dfdmf  5185  dfrnf  5230  nfdm  5233  nfres  5264  dffun6f  5584  dffun6  5585  nffun  5592  nffv  5855  nffvmpt1  5856  dffn5f  5903  funfv2f  5917  fvmpts  5933  fvmpt2i  5938  fvmptss  5940  fvmptex  5942  fvmptdv  5944  fvmptnf  5949  fvmptn  5950  elfvmptrab1  5952  fvopab5  5955  eqfnfv2f  5961  ralrnmpt  6016  f1ompt  6029  ffnfvf  6034  fmptco  6040  fmptcof  6041  fmptcos  6042  funiunfvf  6136  dff13f  6142  f1mpt  6144  fliftfuns  6187  nfiso  6195  csbriota  6244  riota2  6254  riotaxfrd  6262  oprabv  6318  mpt2eq123  6329  cbvmpt2x  6348  cbvmpt2  6349  cbvmpt2v  6350  ovmpt2s  6399  ov2gf  6400  ovmpt2dxf  6401  ovmpt2dx  6402  ovmpt2dv  6408  ovmpt2dv2  6409  ov3  6412  elovmpt2rab  6494  elovmpt2rab1  6495  ovmpt3rab1  6507  ovmpt3rabdm  6508  elovmpt3rab1  6509  nfof  6518  nfofr  6519  offval2  6529  ofrfval2  6530  ofmpteq  6531  onminesb  6606  onminsb  6607  tfis  6662  tfisi  6666  zfrep6  6741  abrexex2g  6750  abrexex2  6754  dfopab2  6827  dfoprab3s  6828  mpt2mptsx  6836  dmmpt2ssx  6838  fmpt2x  6839  fnmpt2ovd  6851  offval22  6852  ovmptss  6854  fmpt2co  6856  dfmpt2  6863  mpt2xopoveq  6939  mpt2xopovel  6940  nftpos  6982  tposoprab  6983  mpt2curryd  6990  mpt2curryvald  6991  fvmpt2curryd  6992  nfrecs  7036  nfrdg  7072  rdgsucmpt2  7088  rdgsucmpt  7089  frsucmpt  7095  frsucmptn  7096  frsucmpt2  7097  oawordeulem  7195  nnawordex  7278  qliftfuns  7390  cbvixpv  7480  nfixp  7481  nfixp1  7482  ixpf  7484  mptelixpg  7499  dom2lem  7548  xpcomco  7600  xpf1o  7672  mapxpen  7676  ac6sfi  7756  iunfi  7800  indexfi  7820  dffi3  7883  nfoi  7931  ixpiunwdom  8009  cantnflem1  8099  cnfcomlem  8134  cnfcomlemOLD  8142  r1val1  8195  rankidb  8209  rankval4  8276  scottex  8294  scottexs  8296  scott0s  8297  cp  8300  tskwe  8322  cardmin2  8370  fseqenlem1  8396  dfac8clem  8404  cardaleph  8461  hsmexlem2  8798  axcc2  8808  ac6num  8850  ac6c4  8852  axdclem  8890  iundom2g  8906  uniimadomf  8911  cardmin  8930  pwfseqlem2  9026  pwfseqlem4a  9028  pwfseqlem4  9029  inar1  9142  lble  10490  nnwof  11149  nnwos  11150  fzrevral  11767  rabssnn0fi  12077  nfseq  12099  seqof2  12147  hashrabsn1  12425  nfwrd  12557  relexpsucnnr  12942  rlim2  13401  ello1mpt  13426  rlimcld2  13483  o1compt  13492  nfsum1  13594  nfsum  13595  sumeq2ii  13597  cbvsumv  13600  cbvsumi  13601  sumfc  13613  summolem2a  13619  zsum  13622  sumss  13628  sumss2  13630  fsumcvg2  13631  fsumzcl2  13642  fsumadd  13643  sumsn  13645  sumsns  13647  fsummsnunz  13651  fsumsplitsnun  13652  fsum2dlem  13667  fsumcom2  13671  fsumshftm  13678  fsummulc2  13681  fsum00  13694  fsumrelem  13703  fsumrlim  13707  fsumo1  13708  o1fsum  13709  fsumiun  13717  prodeq1  13798  nfcprod1  13799  nfcprod  13800  cbvprod  13804  cbvprodv  13805  cbvprodi  13806  prodmolem2a  13823  zprod  13826  fprod  13830  fprodntriv  13831  prodfc  13834  prodss  13836  fprodmul  13847  fproddiv  13848  prodsn  13849  fprodm1s  13856  fprodp1s  13857  prodsns  13858  fprodn0  13865  fprod2dlem  13866  fprodcom2  13870  fprodefsum  13912  prmind2  14312  pcmpt  14495  pcmptdvds  14497  prdsbas3  14970  prdsdsval2  14973  mreiincl  15085  invfuc  15462  yonedalem4b  15744  gsumconstf  17153  gsumsnd  17175  gsumsn  17177  gsumunsnd  17180  gsummpt1n0  17188  gsum2d2lem  17197  gsum2d2  17198  gsumcom2  17199  prdsgsum  17202  prdsgsumOLD  17203  dprd2d2  17288  gsumdixpOLD  17452  gsumdixp  17453  lss1d  17804  psrass1lem  18224  evlslem4OLD  18368  evlslem4  18369  mpfrcl  18382  coe1fzgsumdlem  18538  gsummoncoe1  18541  gsumply1eq  18542  evl1gsumdlem  18587  mdetralt2  19278  mdetunilem2  19282  madugsum  19312  gsummatr01lem4  19327  cayleyhamilton1  19560  neiptopnei  19800  fiuncmp  20071  iuncon  20095  2ndcdisj  20123  dissnlocfin  20196  elptr2  20241  ptbasfi  20248  ptunimpt  20262  ptcldmpt  20281  ptclsg  20282  ptcnplem  20288  ptcnp  20289  cnmpt11  20330  cnmpt1t  20332  cnmpt21  20338  cnmpt2t  20340  cnmptcom  20345  cnmptk2  20353  cnmpt2k  20355  imasnopn  20357  imasncld  20358  imasncls  20359  xkocnv  20481  elmptrab  20494  flfcnp2  20674  ptcmpg  20723  fmucnd  20961  prdsdsf  21036  prdsxmet  21038  cfilucfilOLD  21238  cfilucfil  21239  blval2  21244  restmetu  21256  fsumcn  21540  fsum2cn  21541  ovolfiniun  22078  ovoliunlem3  22081  ovoliun  22082  ovoliun2  22083  ovoliunnul  22084  finiunmbl  22120  volfiniun  22123  iundisj  22124  iundisj2  22125  iunmbl  22129  voliun  22130  iunmbl2  22133  mbfpos  22224  mbfposr  22225  mbfposb  22226  mbfsup  22237  mbfinf  22238  mbflim  22241  i1fposd  22280  itg1climres  22287  itg2splitlem  22321  itg2split  22322  itg2cnlem1  22334  isibl2  22339  itgeq1  22345  nfitg1  22346  nfitg  22347  cbvitg  22348  cbvitgv  22349  itgmpt  22355  itgss3  22387  itgfsum  22399  itgabs  22407  itggt0  22414  itgcn  22415  cbvditgv  22425  limcmpt  22453  limciun  22464  dvmptfsum  22542  dvlipcn  22561  lhop2  22582  dvfsumle  22588  dvfsumabs  22590  dvfsumlem1  22593  dvfsumlem2  22594  dvfsumlem4  22596  dvfsumrlim  22598  dvfsum2  22601  itgparts  22614  itgsubstlem  22615  itgsubst  22616  elplyd  22765  coeeq2  22805  dgrle  22806  ulmss  22958  itgulm2  22970  leibpi  23470  rlimcnp  23493  rlimcnp2  23494  o1cxp  23502  fsumdvdscom  23659  fsumdvdsmul  23669  fsumvma  23686  lgseisenlem2  23823  dchrisumlema  23871  dchrisumlem2  23873  dchrisumlem3  23874  nbgraopALT  24626  cnlnadjlem5  27188  chirred  27512  ralcom4f  27573  rexcom4f  27574  rmo4fOLD  27593  rabtru  27598  iunin1f  27633  iunxsngf  27634  iunxdif3  27637  disji2f  27648  disjorsf  27651  disjif2  27652  disjabrex  27653  disjabrexf  27654  iundisjf  27659  iundisj2f  27660  disjunsn  27664  dfrel4  27668  ac6sf2  27687  dfimafnf  27694  suppss2f  27698  fimarab  27704  fmptdF  27716  resmptf  27719  fvmpt2f  27720  feqmptdf  27723  fmptcof2  27724  fcomptf  27725  acunirnmpt2  27727  acunirnmpt2f  27728  aciunf1lem  27729  aciunf1  27730  offval2f  27733  ofpreima  27734  funcnvmptOLD  27736  funcnvmpt  27737  funcnv5mpt  27738  funcnv4mpt  27739  f1od2  27778  fpwrelmap  27787  fpwrelmapffs  27788  xrofsup  27816  iundisjfi  27835  iundisj2fi  27836  iundisjcnt  27837  iundisj2cnt  27838  nnindf  27844  gsummpt2co  28005  gsumvsca1  28008  gsumvsca2  28009  ordtconlem1  28141  qqhval2  28197  esumcl  28259  nfesum1  28269  nfesum2  28270  cbvesumv  28272  esumid  28273  esumgsum  28274  esumval  28275  esumel  28276  esumnul  28277  esumc  28280  esumrnmpt  28281  esumsplit  28282  esummono  28283  esumpad  28284  esumpad2  28285  esumadd  28286  esumle  28287  gsumesum  28288  esumlub  28289  esumaddf  28290  esumsnf  28293  esumsn  28294  esumpr  28295  esumrnmpt2  28297  esumfzf  28298  esumfsup  28299  esumss  28301  esumpinfval  28302  esumpfinvalf  28305  esumpinfsum  28306  esumpcvgval  28307  esumpmono  28308  esumcocn  28309  esummulc1  28310  esummulc2  28311  esumdivc  28312  esumcvg  28315  esumsup  28318  esumgect  28319  esum2dlem  28321  esum2d  28322  esumiun  28323  sigaclcu2  28350  sigapildsys  28388  measvunilem  28420  measvunilem0  28421  measvuni  28422  measiuns  28425  measiun  28426  meascnbl  28427  voliune  28438  volfiniune  28439  volmeas  28440  ddemeas  28445  imambfm  28470  omscl  28503  oms0  28505  omsmon  28506  omssubadd  28508  carsgclctunlem1  28525  carsggect  28526  carsgclctunlem2  28527  omsmeas  28531  sibfof  28546  eulerpartlemn  28584  lgamgulmlem2  28836  lgamgulmlem6  28840  lgamgulm2  28842  cvmcov  28972  setinds  29450  dfon2lem3  29457  tfisg  29524  wfisg  29529  trpredlem1  29550  trpredtr  29553  trpredmintr  29554  trpred0  29559  trpredrec  29561  frinsg  29565  nfwrecs  29578  nfwlim  29618  sltval2  29656  nobndlem5  29696  finixpnum  30278  ptrest  30288  mbfposadd  30302  dvtanlem  30304  itgabsnc  30324  itggt0cn  30327  ftc1cnnclem  30328  ftc1anclem5  30334  ftc2nc  30339  finminlem  30376  indexa  30464  indexdom  30465  filbcmb  30471  sdclem2  30475  sdclem1  30476  fdc1  30479  totbndbnd  30525  heibor1  30546  scottexf  30816  scott0f  30817  ac6s6f  30821  elrfirn2  30868  mzpsubst  30920  eq0rabdioph  30949  sbcrexgOLD  30958  sbccomieg  30966  rexrabdioph  30967  rexfrabdioph  30968  rabdiophlem2  30975  elnn0rabdioph  30976  dvdsrabdioph  30983  rabrenfdioph  30987  monotoddzz  31118  oddcomabszz  31119  setindtrs  31206  wdom2d2  31216  aomclem6  31244  aomclem8  31246  areaquad  31425  binomcxplemdvbinom  31499  binomcxplemdvsum  31501  binomcxplemnotnn0  31502  compab  31591  evth2f  31630  elunif  31631  fvelrnbf  31633  rfcnpre1  31634  fsumcnf  31636  sumsnd  31641  evthf  31642  refsumcn  31645  rfcnpre2  31646  rfcnpre3  31648  rfcnpre4  31649  rfcnnnub  31651  refsum2cnlem1  31652  refsum2cn  31653  suprnmpt  31691  ssfiunibd  31748  fsumclf  31806  fsumsplitf  31807  fsummulc1f  31808  sumsnf  31809  fsumsplit1  31812  fmul01  31813  fmuldfeqlem1  31815  fmuldfeq  31816  fmul01lt1lem1  31817  fmul01lt1lem2  31818  fmul01lt1  31819  cncfmptss  31820  mulc1cncfg  31822  infrglb  31823  expcnfg  31825  prodsnf  31826  fproddivf  31827  fprodsplitf  31828  fprodcllemf  31830  fprodsplit1f  31832  fprodexp  31839  fprodabs2  31841  fprodle  31843  mccllem  31844  mccl  31845  climmulf  31849  climexp  31850  climsuse  31853  climrecf  31854  climinff  31856  climaddf  31860  mullimc  31861  constlimc  31869  idlimc  31871  limcperiod  31873  sumnnodd  31875  neglimc  31892  addlimc  31893  0ellimcdiv  31894  cncfshift  31915  icccncfext  31929  cncficcgt0  31930  cncfiooicclem1  31935  fprodcncf  31943  dvcosre  31945  dvmptmulf  31973  dvnmptdivc  31974  dvnmul  31979  dvmptfprodlem  31980  dvmptfprod  31981  dvnprodlem1  31982  dvnprodlem2  31983  itgsin0pilem1  31987  ibliccsinexp  31988  itgsinexplem1  31991  itgsinexp  31992  iblsplitf  32008  itgsubsticclem  32013  stoweidlem3  32024  stoweidlem14  32035  stoweidlem16  32037  stoweidlem18  32039  stoweidlem21  32042  stoweidlem23  32044  stoweidlem26  32047  stoweidlem27  32048  stoweidlem28  32049  stoweidlem29  32050  stoweidlem31  32052  stoweidlem34  32055  stoweidlem35  32056  stoweidlem36  32057  stoweidlem41  32062  stoweidlem42  32063  stoweidlem43  32064  stoweidlem46  32067  stoweidlem47  32068  stoweidlem48  32069  stoweidlem51  32072  stoweidlem52  32073  stoweidlem53  32074  stoweidlem54  32075  stoweidlem55  32076  stoweidlem56  32077  stoweidlem57  32078  stoweidlem58  32079  stoweidlem59  32080  stoweidlem60  32081  stoweidlem62  32083  stowei  32085  wallispilem5  32090  stirlinglem4  32098  stirlinglem5  32099  stirlinglem11  32105  stirlinglem12  32106  stirlinglem13  32107  stirlinglem14  32108  stirlinglem15  32109  stirling  32110  fourierdlem20  32148  fourierdlem31  32159  fourierdlem48  32176  fourierdlem51  32179  fourierdlem68  32196  fourierdlem73  32201  fourierdlem79  32207  fourierdlem80  32208  fourierdlem86  32214  fourierdlem89  32217  fourierdlem91  32219  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  fourierdlem115  32243  fourierd  32244  fourierclimd  32245  etransclem2  32258  etransclem24  32280  etransclem25  32281  etransclem26  32282  etransclem28  32284  etransclem32  32288  etransclem35  32291  etransclem37  32293  etransclem44  32300  etransclem46  32302  etransclem48  32304  cbvral2  32416  cbvrex2  32417  raaan2  32419  2reurex  32425  2reu3  32432  2reu7  32435  2reu8  32436  eu2ndop1stv  32446  nfafv  32460  fsummsndifre  32717  fsumsplitsndif  32718  fsummmodsndifre  32719  fsummmodsnunz  32720  opeliun2xp  33176  dmmpt2ssx2  33180  ovmpt2rdxf  33182  ovmpt2rdx  33183  aacllem  33604  iunconlem2  34136  bnj23  34172  bnj1366  34289  bnj1400  34295  bnj1534  34312  bnj1542  34316  bnj607  34375  bnj873  34383  bnj958  34399  bnj1000  34400  bnj981  34409  bnj1014  34419  bnj1123  34443  bnj1204  34469  bnj1388  34490  bnj1398  34491  bnj1408  34493  bnj1445  34501  bnj1446  34502  bnj1447  34503  bnj1448  34504  bnj1449  34505  bnj1466  34510  bnj1467  34511  bnj1463  34512  bnj1312  34515  bnj1498  34518  bnj1519  34522  bnj1520  34523  bnj1525  34526  bnj1529  34527  bj-rabtrALT  34899  fsumshftd  35079  fsumshftdOLD  35080  riotasvd  35084  riotasv2d  35085  riotasv2s  35086  riotaocN  35331  cdleme26ee  36483  cdleme31sn1  36504  cdleme31se2  36506  cdlemefrs29bpre0  36519  cdlemefs32sn1aw  36537  cdleme43fsv1snlem  36543  cdleme41sn3a  36556  cdleme32d  36567  cdleme32f  36569  cdleme40m  36590  cdleme40n  36591  cdleme42b  36601  ltrniotaval  36704  cdlemksv2  36970  cdlemkuv2  36990  cdlemk36  37036  cdlemk38  37038  cdlemkid  37059  cdlemk19x  37066  cdlemk11t  37069  dihglblem5  37422  hlhilset  38061
  Copyright terms: Public domain W3C validator