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

Theorem nfcv 2629
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 1683 . 2  |-  F/ x  y  e.  A
21nfci 2618 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-nf 1600  df-nfc 2617
This theorem is referenced by:  nfcvd  2630  nfelOLD  2643  nfeq1  2644  nfel1  2645  nfeq2  2646  nfel2  2647  nfcvf  2654  r2alOLD  2843  nfra2  2851  r2exOLD  2986  r19.12  2988  ralcom  3022  rexcom  3023  raleq  3058  rexeq  3059  reueq1  3060  rmoeq1  3061  cbvral  3084  cbvrex  3085  rabeq  3107  cbvrabv  3112  vtocl2g  3175  vtoclga  3177  vtocl2ga  3179  vtocl3ga  3181  spcimdv  3195  spcgv  3198  spcegv  3199  rspct  3207  rspc  3208  rspce  3209  rspc2  3222  elabgt  3247  elabf  3249  elabg  3251  elab3g  3256  elrab  3261  2rmorex  3308  nfsbc1v  3351  elrabsf  3370  sbcralt  3412  sbcralg  3415  sbcrex  3416  sbcrexgOLD  3417  sbcreu  3418  sbcreugOLD  3419  cbvcsbv  3441  csbconstg  3448  nfcsb1v  3451  csbie  3461  cbvralcsf  3467  cbvreucsf  3469  cbvrabcsf  3470  cbvralv2  3471  cbvrexv2  3472  n0f  3793  n0  3794  csbnestg  3842  raaan  3935  nfpw  4022  nfop  4229  rabasiun  4329  cbviunv  4364  cbviinv  4365  ssiun2s  4369  iunab  4371  ssiinf  4374  ssiin  4375  iinab  4386  cbvdisjv  4428  disjors  4433  disji2  4434  disjprg  4443  disjxiun  4444  disjxun  4445  cbvmptv  4538  triun  4553  zfrep3cl  4565  csbexg  4579  csbexgOLD  4581  eusvnf  4642  reusv2lem4  4651  reusv2  4653  reusv6OLD  4658  rabxfrd  4668  moop2  4742  euotd  4748  opelopabgf  4767  opelopabf  4772  nfpo  4805  nfso  4806  pofun  4816  nffr  4853  nfse  4854  opeliunxp  5050  nfrel  5086  ralxpf  5147  nfco  5166  nfcnv  5179  dfdmf  5194  dfrnf  5239  nfdm  5242  nfres  5273  dffun6f  5600  dffun6  5601  nffun  5608  nffv  5871  nffvmpt1  5872  dffn5f  5920  funfv2f  5934  fvmpts  5950  fvmpt2i  5954  fvmptss  5956  fvmptex  5958  fvmptdv  5960  fvmptnf  5965  fvmptn  5966  elfvmptrab1  5968  fvopab5  5971  eqfnfv2f  5977  ralrnmpt  6028  f1ompt  6041  ffnfvf  6046  fmptco  6052  fmptcof  6053  fmptcos  6054  funiunfvf  6147  dff13f  6153  f1mpt  6155  fliftfuns  6198  nfiso  6206  csbriota  6255  riota2  6266  riotaxfrd  6274  oprabv  6327  mpt2eq123  6338  cbvmpt2x  6357  cbvmpt2  6358  cbvmpt2v  6359  ovmpt2s  6408  ov2gf  6409  ovmpt2dxf  6410  ovmpt2dx  6411  ovmpt2dv  6417  ovmpt2dv2  6418  ov3  6421  elovmpt2rab  6503  elovmpt2rab1  6504  ovmpt3rab1  6516  ovmpt3rabdm  6517  elovmpt3rab1  6518  nfof  6527  nfofr  6528  offval2  6538  ofrfval2  6539  ofmpteq  6540  onminesb  6611  onminsb  6612  tfis  6667  tfisi  6671  zfrep6  6749  abrexex2g  6758  abrexex2  6762  dfopab2  6835  dfoprab3s  6836  mpt2mptsx  6844  dmmpt2ssx  6846  fmpt2x  6847  fnmpt2ovd  6858  offval22  6859  ovmptss  6861  fmpt2co  6863  dfmpt2  6870  mpt2xopoveq  6944  mpt2xopovel  6945  nftpos  6987  tposoprab  6988  mpt2curryd  6995  mpt2curryvald  6996  fvmpt2curryd  6997  nfrecs  7041  nfrdg  7077  rdgsucmpt2  7093  rdgsucmpt  7094  frsucmpt  7100  frsucmptn  7101  frsucmpt2  7102  oawordeulem  7200  nnawordex  7283  eqerlem  7340  qliftfuns  7395  cbvixpv  7484  nfixp  7485  nfixp1  7486  ixpf  7488  mptelixpg  7503  dom2lem  7552  xpcomco  7604  xpf1o  7676  mapxpen  7680  ac6sfi  7760  iunfi  7804  indexfi  7824  dffi3  7887  nfoi  7935  ixpiunwdom  8013  cantnflem1  8104  cnfcomlem  8139  cnfcomlemOLD  8147  r1val1  8200  rankidb  8214  rankval4  8281  scottex  8299  scottexs  8301  scott0s  8302  cp  8305  tskwe  8327  cardmin2  8375  fseqenlem1  8401  dfac8clem  8409  cardaleph  8466  hsmexlem2  8803  axcc2  8813  ac6num  8855  ac6c4  8857  axdclem  8895  iundom2g  8911  uniimadomf  8916  cardmin  8935  pwfseqlem2  9033  pwfseqlem4a  9035  pwfseqlem4  9036  inar1  9149  lble  10491  nnwof  11144  nnwos  11145  fzrevral  11758  rabssnn0fi  12059  nfseq  12081  seqof2  12129  hashrabsn1  12406  nfwrd  12531  rlim2  13278  ello1mpt  13303  rlimcld2  13360  o1compt  13369  nfsum1  13471  nfsum  13472  sumeq2w  13473  sumeq2ii  13474  cbvsumv  13477  cbvsumi  13478  sumfc  13490  summolem2a  13496  zsum  13499  fsum  13501  sumss  13505  sumss2  13507  fsumcvg2  13508  fsumzcl2  13519  fsumadd  13520  sumsn  13522  sumsns  13524  fsummsnunz  13528  fsumsplitsnun  13529  fsum2dlem  13544  fsumcnv  13547  fsumcom2  13548  fsumshftm  13555  fsum0diag2  13557  fsummulc2  13558  fsum00  13571  fsumrelem  13580  fsumrlim  13584  fsumo1  13585  o1fsum  13586  fsumiun  13594  ruclem1  13821  prmind2  14083  pcmpt  14266  pcmptdvds  14268  prdsbas3  14732  prdsdsval2  14735  mreiincl  14847  invfuc  15197  yonedalem4b  15399  odval  16354  gsumconstf  16746  gsummptshft  16747  gsumsnd  16770  gsumsnf  16771  gsumsn  16772  gsumunsnd  16775  gsummpt1n0  16783  gsum2d2lem  16792  gsum2d2  16793  gsumcom2  16794  prdsgsum  16798  prdsgsumOLD  16799  dprd2d2  16883  gsumdixpOLD  17041  gsumdixp  17042  lss1d  17392  psrass1lem  17800  evlslem4OLD  17944  evlslem4  17945  mpfrcl  17958  coe1fzgsumdlem  18114  gsummoncoe1  18117  gsumply1eq  18118  evl1gsumdlem  18163  mamufval  18654  mdetralt2  18878  mdetunilem2  18882  madugsum  18912  gsummatr01lem4  18927  cayleyhamilton1  19160  neiptopnei  19399  fiuncmp  19670  iuncon  19695  2ndcdisj  19723  elptr2  19810  ptbasfi  19817  ptunimpt  19831  ptcldmpt  19850  ptclsg  19851  ptcnplem  19857  ptcnp  19858  cnmpt11  19899  cnmpt1t  19901  cnmpt21  19907  cnmpt2t  19909  cnmptcom  19914  cnmptk2  19922  cnmpt2k  19924  imasnopn  19926  imasncld  19927  imasncls  19928  xkocnv  20050  elmptrab  20063  flfcnp2  20243  ptcmpg  20292  fmucnd  20530  prdsdsf  20605  prdsxmet  20607  cfilucfilOLD  20807  cfilucfil  20808  blval2  20813  restmetu  20825  fsumcn  21109  fsum2cn  21110  ovolfiniun  21647  ovoliunlem3  21650  ovoliun  21651  ovoliun2  21652  ovoliunnul  21653  finiunmbl  21689  volfiniun  21692  iundisj  21693  iundisj2  21694  iunmbl  21698  voliun  21699  iunmbl2  21702  mbfpos  21793  mbfposr  21794  mbfposb  21795  mbfsup  21806  mbfinf  21807  mbflim  21810  i1fposd  21849  itg1climres  21856  itg2splitlem  21890  itg2split  21891  itg2cnlem1  21903  isibl  21907  isibl2  21908  dfitg  21911  itgeq1  21914  nfitg1  21915  nfitg  21916  cbvitg  21917  cbvitgv  21918  itgmpt  21924  itgss3  21956  itgfsum  21968  itgabs  21976  itggt0  21983  itgcn  21984  cbvditgv  21994  limcmpt  22022  limciun  22033  dvmptfsum  22111  dvlipcn  22130  lhop2  22151  dvfsumle  22157  dvfsumabs  22159  dvfsumlem1  22162  dvfsumlem2  22163  dvfsumlem4  22165  dvfsumrlim  22167  dvfsum2  22170  itgparts  22183  itgsubstlem  22184  itgsubst  22185  elplyd  22334  coeeq2  22374  dgrle  22375  ulmss  22526  itgulm2  22538  leibpi  23001  rlimcnp  23023  rlimcnp2  23024  o1cxp  23032  fsumdvdscom  23189  fsumdvdsmul  23199  fsumvma  23216  lgseisenlem2  23353  dchrisumlema  23401  dchrisumlem2  23403  dchrisumlem3  23404  istrkg2ld  23586  nbgraopALT  24100  cnlnadjlem5  26666  chirred  26990  ralcom4f  27051  rexcom4f  27052  rmo4fOLD  27071  disji2f  27111  disjorsf  27114  disjif2  27115  disjabrex  27116  disjabrexf  27117  disjxpin  27120  iundisjf  27121  iundisj2f  27122  disjunsn  27126  dfrel4  27127  opabdm  27137  opabrn  27138  ssrelf  27139  dfimafnf  27146  suppss2f  27150  fmptdF  27167  resmptf  27169  fvmpt2f  27170  feqmptdf  27173  fmptcof2  27174  fcomptf  27175  offval2f  27178  ofpreima  27179  funcnvmptOLD  27181  funcnvmpt  27182  funcnv5mpt  27183  funcnv4mpt  27184  mpt2mptxf  27190  f1od2  27219  fcobijfs  27221  fpwrelmap  27228  fpwrelmapffs  27229  xrofsup  27250  iundisjfi  27269  iundisj2fi  27270  iundisjcnt  27271  iundisj2cnt  27272  nnindf  27278  gsummpt2co  27434  gsumvsca1  27436  gsumvsca2  27437  ordtconlem1  27542  xrge0tmd  27564  qqhval2  27599  esumcl  27683  nfesum1  27693  cbvesumv  27695  esumid  27696  esumval  27697  esumel  27698  esumnul  27699  esumsplit  27703  esumadd  27704  esumle  27705  esummono  27706  gsumesum  27707  esumlub  27708  esumaddf  27709  esumpr  27713  esumfzf  27715  esumfsup  27716  esumss  27718  esumpinfval  27719  esumpfinvalf  27722  esumpinfsum  27723  esumpcvgval  27724  esumpmono  27725  esumcocn  27726  esummulc1  27727  esummulc2  27728  esumdivc  27729  esumcvg  27732  sigaclcu2  27760  measvunilem  27823  measvunilem0  27824  measvuni  27825  measiuns  27828  measiun  27829  meascnbl  27830  voliune  27841  volfiniune  27842  volmeas  27843  ddemeas  27848  imambfm  27873  oms0  27906  omsmon  27907  sibfof  27922  eulerpartlemn  27960  eulerpart  27961  lgamgulmlem2  28212  lgamgulmlem6  28216  lgamgulm2  28218  cvmcov  28348  relexpsucr  28528  prodeq1  28618  nfcprod1  28619  nfcprod  28620  prodeq2w  28621  cbvprod  28624  cbvprodv  28625  cbvprodi  28626  prodmolem2a  28643  zprod  28646  fprod  28650  fprodntriv  28651  prodfc  28654  prodss  28656  fprodmul  28667  fproddiv  28668  prodsn  28669  fprodm1s  28676  fprodp1s  28677  prodsns  28678  fprodefsum  28681  fprodn0  28686  fprod2dlem  28687  fprodcnv  28690  fprodcom2  28691  setinds  28787  dfon2lem3  28794  tfisg  28861  wfisg  28866  trpredlem1  28887  trpredtr  28890  trpredmintr  28891  trpred0  28896  trpredrec  28898  frinsg  28902  nfwrecs  28915  nfwlim  28955  sltval2  28993  nobndlem5  29033  bpolyval  29388  finixpnum  29615  ptrest  29625  mbfposadd  29639  dvtanlem  29641  itgabsnc  29661  itggt0cn  29664  ftc1cnnclem  29665  ftc1anclem5  29671  ftc2nc  29676  finminlem  29713  indexa  29827  indexdom  29828  filbcmb  29834  sdclem2  29838  sdclem1  29839  fdc1  29842  totbndbnd  29888  heibor1  29909  scottexf  30180  scott0f  30181  ac6s6f  30185  elrfirn2  30232  mzpsubst  30285  eq0rabdioph  30314  sbccomieg  30330  rexrabdioph  30331  rexfrabdioph  30332  rabdiophlem2  30339  elnn0rabdioph  30340  dvdsrabdioph  30347  rabrenfdioph  30352  fphpd  30354  monotuz  30481  monotoddzz  30483  oddcomabszz  30484  setindtrs  30571  wdom2d2  30581  fnwe2val  30599  fnwe2lem1  30600  aomclem6  30609  aomclem8  30611  areaquad  30789  compab  30928  evth2f  30968  elunif  30969  fvelrnbf  30971  rfcnpre1  30972  fsumcnf  30974  sumsnd  30979  evthf  30980  refsumcn  30983  rfcnpre2  30984  rfcnpre3  30986  rfcnpre4  30987  rfcnnnub  30989  refsum2cnlem1  30990  refsum2cn  30991  suprnmpt  31029  upbdrech  31082  ssfiunibd  31086  fmul01  31130  fmuldfeqlem1  31132  fmuldfeq  31133  fmul01lt1lem1  31134  fmul01lt1lem2  31135  fmul01lt1  31136  cncfmptss  31137  mulc1cncfg  31139  infrglb  31140  expcnfg  31142  climmulf  31146  climexp  31147  climsuse  31150  climrecf  31151  climinff  31153  climaddf  31157  mullimc  31158  climf  31164  constlimc  31166  idlimc  31168  limcperiod  31170  sumnnodd  31172  neglimc  31189  addlimc  31190  0ellimcdiv  31191  cncfshift  31212  icccncfext  31226  cncficcgt0  31227  cncfiooicclem1  31232  dvcosre  31239  dvsinax  31241  itgsin0pilem1  31267  ibliccsinexp  31268  itgsinexplem1  31271  itgsinexp  31272  iblsplitf  31288  iblspltprt  31291  itgsubsticclem  31293  itgiccshift  31298  itgperiod  31299  itgsbtaddcnst  31300  stoweidlem3  31303  stoweidlem14  31314  stoweidlem16  31316  stoweidlem18  31318  stoweidlem21  31321  stoweidlem23  31323  stoweidlem26  31326  stoweidlem27  31327  stoweidlem28  31328  stoweidlem29  31329  stoweidlem31  31331  stoweidlem34  31334  stoweidlem35  31335  stoweidlem36  31336  stoweidlem41  31341  stoweidlem42  31342  stoweidlem43  31343  stoweidlem46  31346  stoweidlem47  31347  stoweidlem48  31348  stoweidlem51  31351  stoweidlem52  31352  stoweidlem53  31353  stoweidlem54  31354  stoweidlem55  31355  stoweidlem56  31356  stoweidlem57  31357  stoweidlem58  31358  stoweidlem59  31359  stoweidlem60  31360  stoweidlem62  31362  stowei  31364  wallispilem5  31369  stirlinglem4  31377  stirlinglem5  31378  stirlinglem11  31384  stirlinglem12  31385  stirlinglem13  31386  stirlinglem14  31387  stirlinglem15  31388  stirling  31389  dirkerval  31391  dirkerval2  31394  dirkeritg  31402  dirkercncflem2  31404  dirkercncflem3  31405  dirkercncflem4  31406  dirkercncf  31407  fourierdlem2  31409  fourierdlem3  31410  fourierdlem16  31423  fourierdlem20  31427  fourierdlem21  31428  fourierdlem22  31429  fourierdlem31  31438  fourierdlem48  31455  fourierdlem51  31458  fourierdlem53  31460  fourierdlem68  31475  fourierdlem73  31480  fourierdlem79  31486  fourierdlem80  31487  fourierdlem81  31488  fourierdlem82  31489  fourierdlem86  31493  fourierdlem89  31496  fourierdlem91  31498  fourierdlem92  31499  fourierdlem93  31500  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  fourierdlem115  31522  fourierd  31523  fourierclimd  31524  cbvral2  31644  cbvrex2  31645  raaan2  31647  2reurex  31653  2reu3  31660  2reu7  31663  2reu8  31664  eu2ndop1stv  31674  nfafv  31688  fsummsndifre  31814  fsumsplitsndif  31815  fsummmodsndifre  31816  fsummmodsnunz  31817  opeliun2xp  31986  dmmpt2ssx2  31990  ovmpt2rdxf  31992  ovmpt2rdx  31993  iunconlem2  32815  bnj23  32851  bnj1366  32967  bnj1400  32973  bnj1534  32990  bnj1542  32994  bnj607  33053  bnj873  33061  bnj958  33077  bnj1000  33078  bnj981  33087  bnj1014  33097  bnj1123  33121  bnj1204  33147  bnj1388  33168  bnj1398  33169  bnj1408  33171  bnj1445  33179  bnj1446  33180  bnj1447  33181  bnj1448  33182  bnj1449  33183  bnj1466  33188  bnj1467  33189  bnj1463  33190  bnj1312  33193  bnj1498  33196  bnj1519  33200  bnj1520  33201  bnj1525  33204  bnj1529  33205  bj-rabtrALT  33579  fsumshftd  33754  fsumshftdOLD  33755  riotasvd  33759  riotasv2d  33760  riotasv2s  33761  riotaocN  34006  cdleme26ee  35156  cdleme31sn1  35177  cdleme31se2  35179  cdlemefrs29bpre0  35192  cdlemefs32sn1aw  35210  cdleme43fsv1snlem  35216  cdleme41sn3a  35229  cdleme32d  35240  cdleme32f  35242  cdleme40m  35263  cdleme40n  35264  cdleme42b  35274  ltrniotaval  35377  cdlemksv2  35643  cdlemkuv2  35663  cdlemk36  35709  cdlemk38  35711  cdlemkid  35732  cdlemk19x  35739  cdlemk11t  35742  dihglblem5  36095  hlhilset  36734
  Copyright terms: Public domain W3C validator