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

Theorem nfcv 2569
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 1672 . 2  |-  F/ x  y  e.  A
21nfci 2559 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755   F/_wnfc 2556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-5 1669
This theorem depends on definitions:  df-bi 185  df-nf 1593  df-nfc 2558
This theorem is referenced by:  nfcvd  2570  nfel  2577  nfeq1  2578  nfel1  2579  nfeq2  2580  nfel2  2581  nfcvf  2591  r2al  2742  r2ex  2743  nfra2  2760  r19.12  2820  ralcom  2871  rexcom  2872  raleq  2907  rexeq  2908  reueq1  2909  rmoeq1  2910  cbvral  2933  cbvrex  2934  rabeq  2956  cbvrabv  2961  vtocl2g  3023  vtoclga  3025  vtocl2ga  3027  vtocl3ga  3029  spcimdv  3043  spcgv  3046  spcegv  3047  rspct  3055  rspc  3056  rspce  3057  rspc2  3067  elabgt  3092  elabf  3094  elabg  3096  elab3g  3101  elrab  3106  2rmorex  3152  nfsbc1v  3194  elrabsf  3213  sbcralt  3255  sbcralg  3258  sbcrex  3259  sbcrexgOLD  3260  sbcreu  3261  sbcreugOLD  3262  cbvcsbv  3282  csbconstg  3289  nfcsb1v  3292  cbvralcsf  3307  cbvreucsf  3309  cbvrabcsf  3310  cbvralv2  3311  cbvrexv2  3312  n0f  3633  n0  3634  csbnestg  3682  raaan  3775  nfpw  3860  nfop  4063  cbviunv  4197  cbviinv  4198  ssiun2s  4202  iunab  4204  ssiinf  4207  ssiin  4208  iinab  4219  cbvdisjv  4261  disjors  4266  disji2  4267  disjprg  4276  disjxiun  4277  disjxun  4278  cbvmptv  4371  triun  4386  zfrep3cl  4398  csbexg  4412  csbexgOLD  4414  eusvnf  4475  reusv2lem4  4484  reusv2  4486  reusv6OLD  4491  rabxfrd  4501  moop2  4574  euotd  4580  opelopabf  4602  nfpo  4633  nfso  4634  pofun  4644  nffr  4681  nfse  4682  opeliunxp  4877  nfrel  4912  ralxpf  4973  nfco  4992  nfcnv  5005  dfdmf  5020  dfrnf  5065  nfdm  5068  nfres  5099  dffun6f  5420  dffun6  5421  nffun  5428  nffv  5686  nffvmpt1  5687  dffn5f  5734  funfv2f  5748  fvmpts  5764  fvmpt2i  5768  fvmptss  5770  fvmptex  5772  fvmptdv  5774  fvmptnf  5779  fvmptn  5780  fvopab5  5783  eqfnfv2f  5789  ralrnmpt  5840  f1ompt  5853  ffnfvf  5857  fmptco  5863  fmptcof  5864  fmptcos  5865  funiunfvf  5953  dff13f  5960  f1mpt  5961  fliftfuns  5994  nfiso  6002  csbriota  6052  riota2  6063  riotaxfrd  6071  mpt2eq123  6134  cbvmpt2x  6153  cbvmpt2  6154  cbvmpt2v  6155  ovmpt2s  6203  ov2gf  6204  ovmpt2dxf  6205  ovmpt2dx  6206  ovmpt2dv  6212  ovmpt2dv2  6213  ov3  6216  nfof  6314  nfofr  6315  offval2  6325  ofrfval2  6326  ofmpteq  6327  onminesb  6398  onminsb  6399  tfis  6454  tfisi  6458  zfrep6  6534  abrexex2g  6543  abrexex2  6547  dfopab2  6617  dfoprab3s  6618  mpt2mptsx  6626  dmmpt2ssx  6628  fmpt2x  6629  fnmpt2ovd  6640  offval22  6641  ovmptss  6643  fmpt2co  6645  dfmpt2  6652  mpt2xopoveq  6725  mpt2xopovel  6726  nftpos  6769  tposoprab  6770  nfrecs  6820  nfrdg  6856  rdgsucmpt2  6872  rdgsucmpt  6873  frsucmpt  6879  frsucmptn  6880  frsucmpt2  6881  oawordeulem  6981  nnawordex  7064  eqerlem  7121  qliftfuns  7175  cbvixpv  7269  nfixp  7270  nfixp1  7271  ixpf  7273  mptelixpg  7288  dom2lem  7337  xpcomco  7389  xpf1o  7461  mapxpen  7465  ac6sfi  7544  iunfi  7587  indexfi  7607  dffi3  7669  nfoi  7716  ixpiunwdom  7794  cantnflem1  7885  cnfcomlem  7920  cnfcomlemOLD  7928  r1val1  7981  rankidb  7995  rankval4  8062  scottex  8080  scottexs  8082  scott0s  8083  cp  8086  tskwe  8108  cardmin2  8156  fseqenlem1  8182  dfac8clem  8190  cardaleph  8247  hsmexlem2  8584  axcc2  8594  ac6num  8636  ac6c4  8638  axdclem  8676  iundom2g  8692  uniimadomf  8697  cardmin  8716  pwfseqlem2  8813  pwfseqlem4a  8815  pwfseqlem4  8816  inar1  8929  lble  10269  nnwof  10908  nnwos  10909  fzrevral  11527  nfseq  11799  seqof2  11847  nfwrd  12239  rlim2  12957  ello1mpt  12982  rlimcld2  13039  o1compt  13048  nfsum1  13150  nfsum  13151  sumeq2w  13152  sumeq2ii  13153  cbvsumv  13156  cbvsumi  13157  sumfc  13169  summolem2a  13175  zsum  13178  fsum  13180  sumss  13184  sumss2  13186  fsumcvg2  13187  fsumadd  13198  sumsn  13200  sumsns  13202  fsum2dlem  13220  fsumcnv  13223  fsumcom2  13224  fsumshftm  13230  fsum0diag2  13232  fsummulc2  13233  fsum00  13243  fsumrelem  13252  fsumrlim  13256  fsumo1  13257  o1fsum  13258  fsumiun  13266  ruclem1  13495  prmind2  13756  pcmpt  13936  pcmptdvds  13938  prdsbas3  14401  prdsdsval2  14404  mreiincl  14516  invfuc  14866  yonedalem4b  15068  odval  16016  gsum2d2lem  16438  gsum2d2  16439  gsumcom2  16440  prdsgsum  16444  prdsgsumOLD  16445  dprd2d2  16516  gsumdixpOLD  16634  gsumdixp  16635  lss1d  16965  psrass1lem  17380  evlslem4OLD  17517  evlslem4  17518  mamufval  18124  mdetralt2  18256  mdetunilem2  18260  madugsum  18290  gsummatr01lem4  18305  neiptopnei  18577  fiuncmp  18848  iuncon  18873  2ndcdisj  18901  elptr2  18988  ptbasfi  18995  ptunimpt  19009  ptcldmpt  19028  ptclsg  19029  ptcnplem  19035  ptcnp  19036  cnmpt11  19077  cnmpt1t  19079  cnmpt21  19085  cnmpt2t  19087  cnmptcom  19092  cnmptk2  19100  cnmpt2k  19102  imasnopn  19104  imasncld  19105  imasncls  19106  xkocnv  19228  elmptrab  19241  flfcnp2  19421  ptcmpg  19470  fmucnd  19708  prdsdsf  19783  prdsxmet  19785  cfilucfilOLD  19985  cfilucfil  19986  blval2  19991  restmetu  20003  fsumcn  20287  fsum2cn  20288  ovolfiniun  20825  ovoliunlem3  20828  ovoliun  20829  ovoliun2  20830  ovoliunnul  20831  finiunmbl  20866  volfiniun  20869  iundisj  20870  iundisj2  20871  iunmbl  20875  voliun  20876  iunmbl2  20879  mbfpos  20970  mbfposr  20971  mbfposb  20972  mbfsup  20983  mbfinf  20984  mbflim  20987  i1fposd  21026  itg1climres  21033  itg2splitlem  21067  itg2split  21068  itg2cnlem1  21080  isibl  21084  isibl2  21085  dfitg  21088  itgeq1  21091  nfitg1  21092  nfitg  21093  cbvitg  21094  cbvitgv  21095  itgmpt  21101  itgss3  21133  itgfsum  21145  itgabs  21153  itggt0  21160  itgcn  21161  cbvditgv  21171  limcmpt  21199  limciun  21210  dvmptfsum  21288  dvlipcn  21307  lhop2  21328  dvfsumle  21334  dvfsumabs  21336  dvfsumlem1  21339  dvfsumlem2  21340  dvfsumlem4  21342  dvfsumrlim  21344  dvfsum2  21347  itgparts  21360  itgsubstlem  21361  itgsubst  21362  mpfrcl  21369  elplyd  21554  coeeq2  21594  dgrle  21595  ulmss  21746  itgulm2  21758  leibpi  22221  rlimcnp  22243  rlimcnp2  22244  o1cxp  22252  fsumdvdscom  22409  fsumdvdsmul  22419  fsumvma  22436  lgseisenlem2  22573  dchrisumlema  22621  dchrisumlem2  22623  dchrisumlem3  22624  cnlnadjlem5  25297  chirred  25621  ralcom4f  25682  rexcom4f  25683  rmo4fOLD  25703  disji2f  25744  disjorsf  25747  disjif2  25748  disjabrex  25749  disjabrexf  25750  disjxpin  25753  iundisjf  25754  iundisj2f  25755  disjunsn  25759  dfrel4  25760  opabdm  25766  opabrn  25767  ssrelf  25768  dfimafnf  25773  suppss2f  25777  fmptdF  25795  resmptf  25797  fvmpt2f  25798  feqmptdf  25801  fmptcof2  25802  fcomptf  25803  offval2f  25806  ofpreima  25807  funcnvmptOLD  25809  funcnvmpt  25810  funcnv5mpt  25811  funcnv4mpt  25812  mpt2mptxf  25818  f1od2  25847  fcobijfs  25849  fpwrelmap  25857  fpwrelmapffs  25858  xrofsup  25877  iundisjfi  25902  iundisj2fi  25903  iundisjcnt  25904  iundisj2cnt  25905  nnindf  25911  gsumconstf  26094  gsummpt2co  26100  gsumvsca1  26103  gsumvsca2  26104  ordtconlem1  26207  xrge0tmd  26229  qqhval2  26264  esumcl  26339  nfesum1  26349  cbvesumv  26351  esumid  26352  esumval  26353  esumel  26354  esumnul  26355  esumsplit  26359  esumadd  26360  esumle  26361  esummono  26362  gsumesum  26363  esumlub  26364  esumaddf  26365  esumpr  26369  esumfzf  26371  esumfsup  26372  esumss  26374  esumpinfval  26375  esumpfinvalf  26378  esumpinfsum  26379  esumpcvgval  26380  esumpmono  26381  esumcocn  26382  esummulc1  26383  esummulc2  26384  esumdivc  26385  esumcvg  26388  sigaclcu2  26416  measvunilem  26479  measvunilem0  26480  measvuni  26481  measiuns  26484  measiun  26485  meascnbl  26486  voliune  26498  volfiniune  26499  volmeas  26500  ddemeas  26505  imambfm  26530  sibfof  26573  eulerpartlemn  26611  lgamgulmlem2  26863  lgamgulmlem6  26867  lgamgulm2  26869  cvmcov  26999  relexpsucr  27178  prodeq1  27268  nfcprod1  27269  nfcprod  27270  prodeq2w  27271  cbvprod  27274  cbvprodv  27275  cbvprodi  27276  prodmolem2a  27293  zprod  27296  fprod  27300  fprodntriv  27301  prodfc  27304  prodss  27306  fprodmul  27317  fproddiv  27318  prodsn  27319  fprodm1s  27326  fprodp1s  27327  prodsns  27328  fprodefsum  27331  fprodn0  27336  fprod2dlem  27337  fprodcnv  27340  fprodcom2  27341  setinds  27437  dfon2lem3  27444  tfisg  27511  wfisg  27516  trpredlem1  27537  trpredtr  27540  trpredmintr  27541  trpred0  27546  trpredrec  27548  frinsg  27552  nfwrecs  27565  nfwlim  27605  sltval2  27643  nobndlem5  27683  bpolyval  28038  finixpnum  28255  ptrest  28266  mbfposadd  28280  dvtanlem  28282  itgabsnc  28302  itggt0cn  28305  ftc1cnnclem  28306  ftc1anclem5  28312  ftc2nc  28317  finminlem  28354  indexa  28468  indexdom  28469  filbcmb  28475  sdclem2  28479  sdclem1  28480  fdc1  28483  totbndbnd  28529  heibor1  28550  scottexf  28822  scott0f  28823  ac6s6f  28827  elrfirn2  28874  mzpsubst  28927  eq0rabdioph  28957  sbccomieg  28973  rexrabdioph  28974  rexfrabdioph  28975  rabdiophlem2  28982  elnn0rabdioph  28983  dvdsrabdioph  28990  rabrenfdioph  28995  fphpd  28997  monotuz  29124  monotoddzz  29126  oddcomabszz  29127  setindtrs  29216  wdom2d2  29226  fnwe2val  29244  fnwe2lem1  29245  aomclem6  29254  aomclem8  29256  areaquad  29434  compab  29539  evth2f  29579  elunif  29580  fvelrnbf  29582  rfcnpre1  29583  fsumcnf  29585  sumsnd  29590  evthf  29591  refsumcn  29594  rfcnpre2  29595  rfcnpre3  29597  rfcnpre4  29598  rfcnnnub  29600  refsum2cnlem1  29601  refsum2cn  29602  fmul01  29603  fmuldfeqlem1  29605  fmuldfeq  29606  fmul01lt1lem1  29607  fmul01lt1lem2  29608  fmul01lt1  29609  cncfmptss  29610  mulc1cncfg  29613  infrglb  29614  expcnfg  29616  climmulf  29620  climexp  29621  climsuse  29624  climrecf  29625  climinff  29627  dvcosre  29631  itgsin0pilem1  29633  ibliccsinexp  29634  itgsinexplem1  29637  itgsinexp  29638  stoweidlem3  29641  stoweidlem14  29652  stoweidlem16  29654  stoweidlem18  29656  stoweidlem21  29659  stoweidlem23  29661  stoweidlem26  29664  stoweidlem27  29665  stoweidlem28  29666  stoweidlem29  29667  stoweidlem31  29669  stoweidlem34  29672  stoweidlem35  29673  stoweidlem36  29674  stoweidlem41  29679  stoweidlem42  29680  stoweidlem43  29681  stoweidlem46  29684  stoweidlem47  29685  stoweidlem48  29686  stoweidlem51  29689  stoweidlem52  29690  stoweidlem53  29691  stoweidlem54  29692  stoweidlem55  29693  stoweidlem56  29694  stoweidlem57  29695  stoweidlem58  29696  stoweidlem59  29697  stoweidlem60  29698  stoweidlem62  29700  stowei  29702  wallispilem5  29707  stirlinglem4  29715  stirlinglem5  29716  stirlinglem11  29722  stirlinglem12  29723  stirlinglem13  29724  stirlinglem14  29725  stirlinglem15  29726  stirling  29727  cbvral2  29839  cbvrex2  29840  raaan2  29842  2reurex  29848  2reu3  29855  2reu7  29858  2reu8  29859  eu2ndop1stv  29869  nfafv  29885  opelopabgf  29979  elfvmptrab1  29997  oprabv  30000  elovmpt2rab  30001  elovmpt2rab1  30002  ovmpt3rab1  30004  ovmpt3rabdm  30005  elovmpt3rab1  30006  rabasiun  30073  hashrabsn1  30076  fsumz  30079  fsummsndifre  30080  fsumsplitsndif  30081  fsummmodsndifre  30082  fsummsnunz  30084  fsumsplitsnun  30085  fsummmodsnunre  30086  opeliun2xp  30562  dmmpt2ssx2  30568  ovmpt2rdxf  30570  ovmpt2rdx  30571  iunconlem2  31370  bnj23  31406  bnj1366  31522  bnj1400  31528  bnj1534  31545  bnj1542  31549  bnj607  31608  bnj873  31616  bnj958  31632  bnj1000  31633  bnj981  31642  bnj1014  31652  bnj1123  31676  bnj1204  31702  bnj1388  31723  bnj1398  31724  bnj1408  31726  bnj1445  31734  bnj1446  31735  bnj1447  31736  bnj1448  31737  bnj1449  31738  bnj1466  31743  bnj1467  31744  bnj1463  31745  bnj1312  31748  bnj1498  31751  bnj1519  31755  bnj1520  31756  bnj1525  31759  bnj1529  31760  bj-rabtrALT  32016  riotasvd  32177  riotasv2d  32178  riotasv2s  32179  riotaocN  32424  cdleme26ee  33574  cdleme31sn1  33595  cdleme31se2  33597  cdlemefrs29bpre0  33610  cdlemefs32sn1aw  33628  cdleme43fsv1snlem  33634  cdleme41sn3a  33647  cdleme32d  33658  cdleme32f  33660  cdleme40m  33681  cdleme40n  33682  cdleme42b  33692  ltrniotaval  33795  cdlemksv2  34061  cdlemkuv2  34081  cdlemk36  34127  cdlemk38  34129  cdlemkid  34150  cdlemk19x  34157  cdlemk11t  34160  dihglblem5  34513  hlhilset  35152
  Copyright terms: Public domain W3C validator