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

Theorem nfcv 2548
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 2538 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   F/_wnfc 2535
This theorem is referenced by:  nfcvd  2549  nfel  2556  nfeq1  2557  nfel1  2558  nfeq2  2559  nfel2  2560  nfcvf  2570  r2al  2711  r2ex  2712  nfra2  2728  r19.12  2787  ralcom  2836  rexcom  2837  raleq  2872  rexeq  2873  reueq1  2874  rmoeq1  2875  cbvral  2896  cbvrex  2897  rabeq  2918  cbvrabv  2923  vtoclg  2979  vtocl2g  2983  vtoclga  2985  vtocl2ga  2987  vtocl3ga  2989  spcimdv  3001  spcgv  3004  spcegv  3005  rspct  3013  rspc  3014  rspce  3015  rspc2  3025  ceqsexg  3035  elabgt  3047  elabf  3049  elabg  3051  elab3g  3056  elrab  3060  mob  3084  2rmorex  3106  nfsbc1v  3148  elrabsf  3167  sbcralt  3201  sbcralg  3203  sbcrexg  3204  sbcreug  3205  cbvcsbv  3224  csbexg  3229  csbconstg  3233  nfcsb1v  3251  csbnestg  3269  cbvralcsf  3279  cbvreucsf  3281  cbvrabcsf  3282  cbvralv2  3283  cbvrexv2  3284  n0f  3604  n0  3605  raaan  3703  nfpw  3778  nfop  3968  cbviunv  4098  cbviinv  4099  ssiun2s  4103  iunab  4105  ssiinf  4108  ssiin  4109  iinab  4120  cbvdisjv  4161  disjors  4166  disji2  4167  disjprg  4176  disjxiun  4177  disjxun  4178  cbvmptv  4268  triun  4283  zfrep3cl  4295  moop2  4419  euotd  4425  opelopabf  4447  nfpo  4476  nfso  4477  pofun  4487  nffr  4524  nfse  4525  eusvnf  4685  reusv2lem4  4694  reusv2  4696  reusv6OLD  4701  rabxfrd  4711  onminesb  4745  onminsb  4746  tfis  4801  tfisi  4805  opeliunxp  4896  nfrel  4929  opeliunxp2  4980  ralxpf  4986  nfco  5005  nfcnv  5018  dfdmf  5031  dfrnf  5075  nfdm  5078  nfres  5115  dffun6f  5435  dffun6  5436  nffun  5443  nffv  5702  nffvmpt1  5703  dffn5f  5748  funfv2f  5759  fvmpts  5774  fvmpt2i  5778  fvmptss  5780  fvmptex  5782  fvmptdv  5784  fvmptnf  5789  fvmptn  5790  eqfnfv2f  5798  ralrnmpt  5845  f1ompt  5858  ffnfvf  5862  fmptco  5868  fmptcof  5869  fmptcos  5870  zfrep6  5935  abrexex2g  5955  funiunfvf  5963  abrexex2  5968  dff13f  5973  f1mpt  5974  fliftfuns  6003  nfiso  6011  mpt2eq123  6100  cbvmpt2x  6117  cbvmpt2  6118  cbvmpt2v  6119  ovmpt2s  6164  ov2gf  6165  ovmpt2dxf  6166  ovmpt2dx  6167  ovmpt2dv  6173  ovmpt2dv2  6174  ov3  6177  nfof  6277  nfofr  6278  offval2  6289  ofrfval2  6290  dfopab2  6368  dfoprab3s  6369  mpt2mptsx  6381  dmmpt2ssx  6383  fmpt2x  6384  ovmptss  6395  fmpt2co  6397  dfmpt2  6404  mpt2xopoveq  6437  mpt2xopovel  6438  nftpos  6481  tposoprab  6482  fvopab5  6501  nfriota1  6524  csbriotag  6529  riota2  6539  riotaxfrd  6548  riotasvd  6559  riotasvdOLD  6560  riotasv2d  6561  riotasv2dOLD  6562  riotasv2s  6563  riotasv3dOLD  6566  nfrecs  6602  nfrdg  6639  rdgsucmpt2  6655  rdgsucmpt  6656  frsucmpt  6662  frsucmptn  6663  frsucmpt2  6664  oawordeulem  6764  nnawordex  6847  eqerlem  6904  qliftfuns  6958  cbvixpv  7047  nfixp  7048  nfixp1  7049  ixpf  7051  mptelixpg  7066  dom2lem  7114  xpcomco  7165  xpf1o  7236  mapxpen  7240  ac6sfi  7318  iunfi  7361  indexfi  7380  dffi3  7402  nfoi  7447  ixpiunwdom  7523  cnfcomlem  7620  r1val1  7676  rankidb  7690  rankval4  7757  scottex  7773  scottexs  7775  scott0s  7776  cp  7779  tskwe  7801  cardmin2  7849  fseqenlem1  7869  dfac8clem  7877  cardaleph  7934  hsmexlem2  8271  axcc2  8281  ac6num  8323  ac6c4  8325  axdclem  8363  iundom2g  8379  uniimadomf  8384  cardmin  8403  pwfseqlem2  8498  pwfseqlem4a  8500  pwfseqlem4  8501  inar1  8614  lble  9924  nnwof  10507  nnwos  10508  fzrevral  11094  nfseq  11296  seqof2  11344  nfwrd  11703  rlim2  12253  ello1mpt  12278  rlimcld2  12335  o1compt  12344  sumeq1  12446  nfsum1  12447  nfsum  12448  sumeq2w  12449  cbvsum  12452  cbvsumv  12453  cbvsumi  12454  sumfc  12466  summolem2a  12472  zsum  12475  fsum  12477  sumss  12481  sumss2  12483  fsumcvg2  12484  fsumadd  12495  sumsn  12497  sumsns  12499  fsum2dlem  12517  fsumcnv  12520  fsumcom2  12521  fsumshftm  12527  fsum0diag2  12529  fsummulc2  12530  fsum00  12540  fsumrelem  12549  fsumrlim  12553  fsumo1  12554  o1fsum  12555  fsumiun  12563  ruclem1  12793  prmind2  13053  pcmpt  13224  pcmptdvds  13226  prdsbas3  13666  prdsdsval2  13669  mreiincl  13784  invfuc  14134  yonedalem4b  14336  odval  15135  gsum2d2lem  15510  gsum2d2  15511  gsumcom2  15512  prdsgsum  15515  dprd2d2  15565  gsumdixp  15678  lss1d  16002  psrass1lem  16405  evlslem4  16527  neiptopnei  17159  fiuncmp  17429  iuncon  17452  2ndcdisj  17480  elptr2  17567  ptbasfi  17574  ptunimpt  17588  ptcldmpt  17607  ptclsg  17608  ptcnplem  17614  ptcnp  17615  cnmpt11  17656  cnmpt1t  17658  cnmpt21  17664  cnmpt2t  17666  cnmptcom  17671  cnmptk2  17679  cnmpt2k  17681  imasnopn  17683  imasncld  17684  imasncls  17685  xkocnv  17807  elmptrab  17820  flfcnp2  18000  ptcmpg  18049  cnextfvval  18057  fmucnd  18283  prdsdsf  18358  prdsxmet  18360  cfilucfilOLD  18560  cfilucfil  18561  blval2  18566  restmetu  18578  fsumcn  18861  fsum2cn  18862  ovolfiniun  19358  ovoliunlem3  19361  ovoliun  19362  ovoliun2  19363  ovoliunnul  19364  finiunmbl  19399  volfiniun  19402  iundisj  19403  iundisj2  19404  iunmbl  19408  voliun  19409  iunmbl2  19412  mbfpos  19504  mbfposr  19505  mbfposb  19506  mbfsup  19517  mbfinf  19518  mbflim  19521  i1fposd  19560  itg1climres  19567  itg2splitlem  19601  itg2split  19602  itg2cnlem1  19614  isibl  19618  isibl2  19619  dfitg  19622  itgeq1  19625  nfitg1  19626  nfitg  19627  cbvitg  19628  cbvitgv  19629  itgmpt  19635  itgss3  19667  itgfsum  19679  itgabs  19687  itggt0  19694  itgcn  19695  cbvditgv  19703  limcmpt  19731  limciun  19742  dvmptfsum  19820  dvlipcn  19839  lhop2  19860  dvfsumle  19866  dvfsumabs  19868  dvfsumlem1  19871  dvfsumlem2  19872  dvfsumlem4  19874  dvfsumrlim  19876  dvfsum2  19879  itgparts  19892  itgsubstlem  19893  itgsubst  19894  mpfrcl  19900  elplyd  20082  coeeq2  20122  dgrle  20123  ulmss  20274  itgulm2  20286  leibpi  20743  rlimcnp  20765  rlimcnp2  20766  o1cxp  20774  fsumdvdscom  20931  fsumdvdsmul  20941  fsumvma  20958  lgseisenlem2  21095  dchrisumlema  21143  dchrisumlem2  21145  dchrisumlem3  21146  cnlnadjlem5  23535  chirred  23859  ralcom4f  23926  rexcom4f  23927  rmo4fOLD  23944  disji2f  23980  disjorsf  23983  disjif2  23984  disjabrex  23985  disjabrexf  23986  disjxpin  23989  iundisjf  23990  iundisj2f  23991  dfrel4  23995  dfimafnf  24004  suppss2f  24010  fmptdF  24030  resmptf  24032  fvmpt2f  24033  feqmptdf  24036  fmptcof2  24037  fcomptf  24038  offval2f  24041  ofpreima  24042  funcnvmptOLD  24043  funcnvmpt  24044  funcnv5mpt  24045  funcnv4mpt  24046  xrofsup  24087  iundisjfi  24113  iundisj2fi  24114  iundisjcnt  24115  iundisj2cnt  24116  gsumconstf  24183  xrge0tmd  24293  qqhval2  24327  esumcl  24388  nfesum1  24398  cbvesumv  24400  esumid  24401  esumval  24402  esumel  24403  esumnul  24404  esumsplit  24408  esumadd  24409  esumle  24410  esummono  24411  gsumesum  24412  esumlub  24413  esumaddf  24414  esumpr  24418  esumfzf  24420  esumfsup  24421  esumss  24423  esumpinfval  24424  esumpfinvalf  24427  esumpinfsum  24428  esumpcvgval  24429  esumpmono  24430  esumcocn  24431  esummulc1  24432  esummulc2  24433  esumdivc  24434  esumcvg  24437  sigaclcu2  24464  measvunilem  24527  measvunilem0  24528  measvuni  24529  measiuns  24532  measiun  24533  meascnbl  24534  voliune  24546  volfiniune  24547  volmeas  24548  imambfm  24573  sibfof  24615  lgamgulmlem2  24775  lgamgulmlem6  24779  lgamgulm2  24781  cvmcov  24911  relexpsucr  25091  prodeq1  25196  nfcprod1  25197  nfcprod  25198  prodeq2w  25199  cbvprod  25202  cbvprodv  25203  cbvprodi  25204  prodmolem2a  25221  zprod  25224  fprod  25228  fprodntriv  25229  prodfc  25232  prodss  25234  fprodmul  25245  fproddiv  25246  prodsn  25247  fprodm1s  25254  fprodp1s  25255  prodsns  25256  fprodefsum  25259  fprodn0  25264  fprod2dlem  25265  fprodcnv  25268  fprodcom2  25269  setinds  25356  dfon2lem3  25363  tfisg  25426  wfisg  25431  trpredlem1  25452  trpredtr  25455  trpredmintr  25456  trpred0  25461  trpredrec  25463  frinsg  25467  sltval2  25532  nobndlem5  25572  bpolyval  26007  mbfposadd  26161  itgabsnc  26181  itggt0cn  26184  ftc1cnnclem  26185  finminlem  26219  indexa  26333  indexdom  26334  filbcmb  26340  sdclem2  26344  sdclem1  26345  fdc1  26348  totbndbnd  26396  heibor1  26417  elrfirn2  26648  ofmpteq  26674  mzpsubst  26703  eq0rabdioph  26733  sbccomieg  26747  rexrabdioph  26752  rexfrabdioph  26753  rabdiophlem2  26760  elnn0rabdioph  26761  dvdsrabdioph  26768  rabrenfdioph  26773  fphpd  26775  monotuz  26902  monotoddzz  26904  oddcomabszz  26905  setindtrs  26994  wdom2d2  27004  fnwe2val  27022  fnwe2lem1  27023  aomclem6  27032  aomclem8  27035  mamufval  27319  compab  27519  evth2f  27561  elunif  27562  fvelrnbf  27564  rfcnpre1  27565  fsumcnf  27567  sumsnd  27572  evthf  27573  refsumcn  27576  rfcnpre2  27577  rfcnpre3  27579  rfcnpre4  27580  rfcnnnub  27582  refsum2cnlem1  27583  refsum2cn  27584  fmul01  27585  fmuldfeqlem1  27587  fmuldfeq  27588  fmul01lt1lem1  27589  fmul01lt1lem2  27590  fmul01lt1  27591  cncfmptss  27592  mulc1cncfg  27596  infrglb  27597  expcnfg  27601  climmulf  27605  climexp  27606  climsuse  27609  climrecf  27610  climinff  27612  dvcosre  27616  itgsin0pilem1  27619  ibliccsinexp  27620  itgsinexplem1  27623  itgsinexp  27624  stoweidlem3  27627  stoweidlem14  27638  stoweidlem16  27640  stoweidlem18  27642  stoweidlem21  27645  stoweidlem23  27647  stoweidlem26  27650  stoweidlem27  27651  stoweidlem28  27652  stoweidlem29  27653  stoweidlem31  27655  stoweidlem34  27658  stoweidlem35  27659  stoweidlem36  27660  stoweidlem41  27665  stoweidlem42  27666  stoweidlem43  27667  stoweidlem46  27670  stoweidlem47  27671  stoweidlem48  27672  stoweidlem51  27675  stoweidlem52  27676  stoweidlem53  27677  stoweidlem54  27678  stoweidlem55  27679  stoweidlem56  27680  stoweidlem57  27681  stoweidlem58  27682  stoweidlem59  27683  stoweidlem60  27684  stoweidlem62  27686  stowei  27688  wallispilem5  27693  stirlinglem4  27701  stirlinglem5  27702  stirlinglem11  27708  stirlinglem12  27709  stirlinglem13  27710  stirlinglem14  27711  stirlinglem15  27712  stirling  27713  cbvral2  27825  cbvrex2  27826  raaan2  27828  2reurex  27834  2reu3  27841  2reu7  27844  2reu8  27845  eu2ndop1stv  27855  nfafv  27875  iunconlem2  28766  bnj23  28801  bnj1366  28919  bnj1400  28925  bnj1534  28942  bnj1542  28946  bnj607  29005  bnj873  29013  bnj958  29029  bnj1000  29030  bnj981  29039  bnj1014  29049  bnj1123  29073  bnj1204  29099  bnj1388  29120  bnj1398  29121  bnj1408  29123  bnj1445  29131  bnj1446  29132  bnj1447  29133  bnj1448  29134  bnj1449  29135  bnj1466  29140  bnj1467  29141  bnj1463  29142  bnj1312  29145  bnj1498  29148  bnj1519  29152  bnj1520  29153  bnj1525  29156  bnj1529  29157  riotaocN  29704  cdleme26ee  30854  cdleme31sn1  30875  cdleme31se2  30877  cdlemefrs29bpre0  30890  cdlemefs32sn1aw  30908  cdleme43fsv1snlem  30914  cdleme41sn3a  30927  cdleme32d  30938  cdleme32f  30940  cdleme40m  30961  cdleme40n  30962  cdleme42b  30972  ltrniotaval  31075  cdlemksv2  31341  cdlemkuv2  31361  cdlemk36  31407  cdlemk38  31409  cdlemkid  31430  cdlemk19x  31437  cdlemk11t  31440  dihglblem5  31793  hlhilset  32432
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 2537
  Copyright terms: Public domain W3C validator