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

Theorem nfcv 2494
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 1619 . 2  |-  F/ x  y  e.  A
21nfci 2484 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    e. wcel 1710   F/_wnfc 2481
This theorem is referenced by:  nfcvd  2495  nfel  2502  nfeq1  2503  nfel1  2504  nfeq2  2505  nfel2  2506  nfcvf  2516  r2al  2656  r2ex  2657  nfra2  2673  r19.12  2732  ralcom  2776  rexcom  2777  raleq  2812  rexeq  2813  reueq1  2814  rmoeq1  2815  cbvral  2836  cbvrex  2837  rabeq  2858  cbvrabv  2863  vtoclg  2919  vtocl2g  2923  vtoclga  2925  vtocl2ga  2927  vtocl3ga  2929  spcimdv  2941  spcgv  2944  spcegv  2945  rspct  2953  rspc  2954  rspce  2955  rspc2  2965  ceqsexg  2975  elabgt  2987  elabf  2989  elabg  2991  elab3g  2996  elrab  2999  mob  3023  2rmorex  3045  nfsbc1v  3086  elrabsf  3105  sbcralt  3139  sbcralg  3141  sbcrexg  3142  sbcreug  3143  cbvcsbv  3162  csbexg  3167  csbconstg  3171  nfcsb1v  3189  csbnestg  3207  cbvralcsf  3219  cbvreucsf  3221  cbvrabcsf  3222  cbvralv2  3223  cbvrexv2  3224  n0f  3539  n0  3540  raaan  3637  nfpw  3712  nfop  3893  cbviunv  4022  cbviinv  4023  ssiun2s  4027  iunab  4029  ssiinf  4032  ssiin  4033  iinab  4044  cbvdisjv  4085  disjors  4090  disji2  4091  disjprg  4100  disjxiun  4101  disjxun  4102  cbvmptv  4192  triun  4207  zfrep3cl  4219  moop2  4343  euotd  4349  opelopabf  4371  nfpo  4401  nfso  4402  pofun  4412  nffr  4449  nfse  4450  eusvnf  4611  reusv2lem4  4620  reusv2  4622  reusv6OLD  4627  rabxfrd  4637  onminesb  4671  onminsb  4672  tfis  4727  tfisi  4731  opeliunxp  4822  nfrel  4856  opeliunxp2  4906  ralxpf  4912  nfco  4931  nfcnv  4942  dfdmf  4955  dfrnf  4999  nfdm  5002  nfres  5039  dffun6f  5351  dffun6  5352  nffun  5359  nffv  5615  nffvmpt1  5616  dffn5f  5660  funfv2f  5671  fvmpts  5686  fvmpt2i  5690  fvmptss  5692  fvmptex  5693  fvmptdv  5695  fvmptt  5698  fvmptnf  5700  fvmptn  5701  eqfnfv2f  5709  ralrnmpt  5752  f1ompt  5765  ffnfvf  5769  fmptco  5774  fmptcof  5775  fmptcos  5776  zfrep6  5834  abrexex2g  5854  funiunfvf  5862  abrexex2  5867  dff13f  5871  f1mpt  5872  fliftfuns  5900  nfiso  5908  mpt2eq123  5994  cbvmpt2x  6011  cbvmpt2  6012  cbvmpt2v  6013  ovmpt2s  6058  ov2gf  6059  ovmpt2dxf  6060  ovmpt2dx  6061  ovmpt2dv  6067  ovmpt2dv2  6068  ov3  6071  nfof  6170  nfofr  6171  offval2  6182  ofrfval2  6183  dfopab2  6261  dfoprab3s  6262  mpt2mptsx  6274  dmmpt2ssx  6276  fmpt2x  6277  ovmptss  6287  fmpt2co  6289  dfmpt2  6296  nftpos  6356  tposoprab  6357  fvopab5  6376  opabiota  6380  nfriota1  6399  csbriotag  6404  riota2  6414  riotaxfrd  6423  riotasvd  6434  riotasvdOLD  6435  riotasv2d  6436  riotasv2dOLD  6437  riotasv2s  6438  riotasv3dOLD  6441  nfrecs  6477  nfrdg  6514  rdgsucmpt2  6530  rdgsucmpt  6531  frsucmpt  6537  frsucmptn  6538  frsucmpt2  6539  oawordeulem  6639  nnawordex  6722  eqerlem  6779  qliftfuns  6833  cbvixpv  6922  nfixp  6923  nfixp1  6924  ixpf  6926  mptelixpg  6941  dom2lem  6989  xpcomco  7040  xpf1o  7111  mapxpen  7115  ac6sfi  7191  iunfi  7234  indexfi  7253  dffi3  7274  nfoi  7319  ixpiunwdom  7395  cnfcomlem  7492  r1val1  7548  rankidb  7562  rankval4  7629  scottex  7645  scottexs  7647  scott0s  7648  cp  7651  tskwe  7673  cardmin2  7721  fseqenlem1  7741  dfac8clem  7749  acni2  7763  cardaleph  7806  hsmexlem2  8143  axcc2  8153  ac6num  8196  ac6c4  8198  axdclem  8236  iundom2g  8252  uniimadomf  8257  cardmin  8276  pwfseqlem2  8371  pwfseqlem4a  8373  pwfseqlem4  8374  inar1  8487  lble  9796  nnwof  10377  nnwos  10378  fzrevral  10958  nfseq  11148  seqof2  11196  nfwrd  11522  rlim2  12066  ello1mpt  12091  rlimcld2  12148  o1compt  12157  sumeq1  12259  nfsum1  12260  nfsum  12261  sumeq2w  12262  cbvsum  12265  cbvsumv  12266  cbvsumi  12267  sumfc  12279  summolem2a  12285  zsum  12288  fsum  12290  fsumf1o  12293  sumss  12294  sumss2  12296  fsumcvg2  12297  fsumadd  12308  sumsn  12310  sumsns  12312  isummulc2  12322  fsum2dlem  12330  fsumcnv  12333  fsumcom2  12334  fsumshftm  12340  fsum0diag2  12342  fsummulc2  12343  fsum00  12353  fsumrelem  12362  fsumrlim  12366  fsumo1  12367  o1fsum  12368  fsumiun  12376  isumshft  12395  ruclem1  12606  prmind2  12866  iserodd  12985  pcmpt  13037  pcmptdvds  13039  prdsbas3  13479  prdsdsval2  13482  mreiincl  13597  invfuc  13947  yonedalem4b  14149  odval  14948  gsum2d2lem  15323  gsum2d2  15324  gsumcom2  15325  prdsgsum  15328  dprdwd  15345  dprd2d2  15378  gsumdixp  15491  lss1d  15819  psrass1lem  16222  evlslem4  16344  fiuncmp  17237  iuncon  17260  2ndcdisj  17288  elptr2  17375  ptbasfi  17382  ptunimpt  17396  ptcldmpt  17414  ptclsg  17415  txcnp  17420  ptcnplem  17421  ptcnp  17422  cnmpt11  17463  cnmpt1t  17465  cnmpt21  17471  cnmpt2t  17473  cnmptcom  17478  cnmptk2  17486  cnmpt2k  17488  xkocnv  17611  elmptrab  17624  flfcnp2  17804  ptcmpg  17853  prdsdsf  18033  prdsxmet  18035  fsumcn  18477  fsum2cn  18478  ovolfiniun  18964  ovoliunlem3  18967  ovoliun  18968  ovoliun2  18969  ovoliunnul  18970  finiunmbl  19005  volfiniun  19008  iundisj  19009  iundisj2  19010  iunmbl  19014  voliun  19015  iunmbl2  19018  mbfeqalem  19101  mbfpos  19110  mbfposr  19111  mbfposb  19112  mbfsup  19123  mbfinf  19124  mbflim  19127  i1fposd  19166  itg1climres  19173  itg2splitlem  19207  itg2split  19208  itg2cnlem1  19220  isibl  19224  isibl2  19225  dfitg  19228  itgeq1  19231  nfitg1  19232  nfitg  19233  cbvitg  19234  cbvitgv  19235  itgmpt  19241  itgeqa  19272  itgss3  19273  itgfsum  19285  itgabs  19293  itggt0  19300  itgcn  19301  cbvditgv  19309  limcmpt  19337  limciun  19348  dvmptfsum  19426  dvlipcn  19445  lhop2  19466  dvfsumle  19472  dvfsumabs  19474  dvfsumlem1  19477  dvfsumlem2  19478  dvfsumlem4  19480  dvfsumrlim  19482  dvfsum2  19485  itgparts  19498  itgsubstlem  19499  itgsubst  19500  mpfrcl  19506  elplyd  19688  coeeq2  19728  dgrle  19729  ulmss  19880  itgulm2  19892  leibpi  20349  rlimcnp  20371  rlimcnp2  20372  o1cxp  20380  fsumdvdscom  20537  fsumdvdsmul  20547  fsumvma  20564  lgseisenlem2  20701  dchrisumlema  20749  dchrisumlem2  20751  dchrisumlem3  20752  cnlnadjlem5  22765  chirred  23089  ralcom4f  23154  rexcom4f  23155  clelsb3f  23166  rmo3f  23177  rmo4fOLD  23178  abrexss  23189  ifeqeqx  23200  cbvdisjf  23214  disji2f  23218  disjorf  23220  disjorsf  23221  disjif2  23222  disjabrex  23223  disjabrexf  23224  iundisjf  23227  iundisj2f  23228  dfrel4  23242  dfimafnf  23247  suppss2f  23253  ofrn2  23257  cbvmptf  23271  fmptdF  23272  fmpt3d  23273  resmptf  23274  fvmpt2f  23275  feqmptdf  23279  fmptcof2  23280  fcomptf  23281  offval2f  23284  funcnvmptOLD  23285  funcnvmpt  23286  funcnv5mpt  23287  funcnv4mpt  23288  xrofsup  23327  iundisjfi  23356  iundisj2fi  23357  iundisjcnt  23358  iundisj2cnt  23359  hashunif  23362  gsumconstf  23414  neiptopnei  23445  neiptopreu  23446  xrge0mulc1cn  23483  xrge0tmdALT  23487  xrge0tmd  23488  cnextfvval  23502  cnextf  23503  ustuqtop  23550  utopsnneiplem  23551  fmucnd  23586  cfilucfil  23603  blval2  23608  restmetu  23615  qqhval2  23639  esumcl  23693  nfesum1  23703  cbvesumv  23705  esumid  23706  esumval  23707  esumel  23708  esumnul  23709  esum0  23710  esumsplit  23713  esumadd  23714  esumle  23715  esummono  23716  gsumesum  23717  esumlub  23718  esumaddf  23719  esumcst  23721  esumpr  23723  esumfzf  23725  esumfsup  23726  esumss  23728  esumpinfval  23729  esumpfinval  23731  esumpfinvalf  23732  esumpinfsum  23733  esumpcvgval  23734  esumpmono  23735  esumcocn  23736  esummulc1  23737  esummulc2  23738  esumdivc  23739  esumcvg  23742  sigaclcuni  23767  sigaclcu2  23769  measvunilem  23830  measvunilem0  23831  measvuni  23832  measiuns  23835  measiun  23836  meascnbl  23837  voliune  23849  volfiniune  23850  volmeas  23851  imambfm  23876  rrvadd  23959  ballotlemelo  23994  ballotleme  24003  ballotlemi  24007  ballotlemsval  24015  ballotlemsv  24016  ballotlemrval  24024  ballotlemrinv  24040  lgamgulmlem2  24063  lgamgulmlem6  24067  lgamgulm2  24069  lgamcvglem  24073  cvmcov  24198  cvmliftphtlem  24252  relexpsucr  24430  dedekind  24488  dedekindle  24489  prodeq1  24536  nfcprod1  24537  nfcprod  24538  prodeq2w  24539  cbvprod  24542  cbvprodv  24543  cbvprodi  24544  prodmolem2a  24561  zprod  24564  fprod  24568  fprodntriv  24569  prodfc  24572  fprodf1o  24573  prodss  24574  fprodmul  24585  fproddiv  24586  prodsn  24587  fprodm1s  24594  fprodp1s  24595  prodsns  24596  fprodefsum  24599  fprodn0  24604  setinds  24692  dfon2lem3  24699  tfisg  24762  wfisg  24767  trpredlem1  24788  trpredtr  24791  trpredmintr  24792  trpred0  24797  trpredrec  24799  frinsg  24803  sltval2  24868  nobndlem5  24908  bpolyval  25343  itgaddnclem2  25499  itgabsnc  25509  itggt0cn  25512  ftc1cnnclem  25513  finminlem  25555  indexa  25736  indexdom  25737  filbcmb  25756  sdclem2  25776  sdclem1  25777  fdc1  25780  totbndbnd  25836  heibor1  25857  elrfirn2  26094  ofmpteq  26120  mzpsubst  26149  eq0rabdioph  26179  sbccomieg  26193  rexrabdioph  26198  rexfrabdioph  26199  rabdiophlem2  26206  elnn0rabdioph  26207  dvdsrabdioph  26214  rabrenfdioph  26220  fphpd  26222  monotuz  26349  monotoddzz  26351  oddcomabszz  26352  setindtrs  26441  wdom2d2  26451  fnwe2val  26469  fnwe2lem1  26470  aomclem6  26479  aomclem8  26482  flcidc  26702  mamufval  26766  compab  26967  evth2f  27009  elunif  27010  fvelrnbf  27012  rfcnpre1  27013  fsumcnf  27015  sumsnd  27020  evthf  27021  refsumcn  27024  rfcnpre2  27025  rfcnpre3  27027  rfcnpre4  27028  rfcnnnub  27030  refsum2cnlem1  27031  refsum2cn  27032  fmul01  27033  fmuldfeqlem1  27035  fmuldfeq  27036  fmul01lt1lem1  27037  fmul01lt1lem2  27038  fmul01lt1  27039  cncfmptss  27040  mulc1cncfg  27044  infrglb  27045  expcnfg  27049  climmulf  27053  climexp  27054  climsuse  27057  climrecf  27058  climinff  27060  dvcosre  27064  itgsin0pilem1  27067  ibliccsinexp  27068  itgsinexplem1  27071  itgsinexp  27072  stoweidlem3  27075  stoweidlem8  27080  stoweidlem14  27086  stoweidlem16  27088  stoweidlem18  27090  stoweidlem19  27091  stoweidlem21  27093  stoweidlem22  27094  stoweidlem23  27095  stoweidlem26  27098  stoweidlem27  27099  stoweidlem28  27100  stoweidlem29  27101  stoweidlem30  27102  stoweidlem31  27103  stoweidlem32  27104  stoweidlem34  27106  stoweidlem35  27107  stoweidlem36  27108  stoweidlem41  27113  stoweidlem42  27114  stoweidlem43  27115  stoweidlem44  27116  stoweidlem45  27117  stoweidlem46  27118  stoweidlem47  27119  stoweidlem48  27120  stoweidlem49  27121  stoweidlem51  27123  stoweidlem52  27124  stoweidlem53  27125  stoweidlem54  27126  stoweidlem55  27127  stoweidlem56  27128  stoweidlem57  27129  stoweidlem58  27130  stoweidlem59  27131  stoweidlem60  27132  stoweidlem62  27134  stowei  27136  wallispilem5  27141  wallispi  27142  stirlinglem2  27147  stirlinglem3  27148  stirlinglem4  27149  stirlinglem5  27150  stirlinglem8  27153  stirlinglem11  27156  stirlinglem12  27157  stirlinglem13  27158  stirlinglem14  27159  stirlinglem15  27160  stirling  27161  cbvral2  27273  cbvrex2  27274  raaan2  27276  2reurex  27282  2reu3  27289  2reu7  27292  2reu8  27293  eu2ndop1stv  27303  nfafv  27324  mpt2xopoveq  27442  mpt2xopovel  27443  bnj23  28506  bnj1366  28624  bnj1379  28625  bnj1400  28630  bnj1534  28647  bnj1542  28651  bnj607  28710  bnj873  28718  bnj958  28734  bnj1000  28735  bnj981  28744  bnj1014  28754  bnj1123  28778  bnj1204  28804  bnj1388  28825  bnj1398  28826  bnj1408  28828  bnj1445  28836  bnj1446  28837  bnj1447  28838  bnj1448  28839  bnj1449  28840  bnj1466  28845  bnj1467  28846  bnj1463  28847  bnj1312  28850  bnj1498  28853  bnj1519  28857  bnj1520  28858  bnj1525  28861  bnj1529  28862  riotaocN  29468  cdleme26ee  30618  cdleme31sn1  30639  cdleme31se2  30641  cdlemefrs29bpre0  30654  cdlemefs32sn1aw  30672  cdleme43fsv1snlem  30678  cdleme41sn3a  30691  cdleme32d  30702  cdleme32f  30704  cdleme40m  30725  cdleme40n  30726  cdleme42b  30736  ltrniotaval  30839  cdlemksv2  31105  cdlemkuv2  31125  cdlemk36  31171  cdlemk38  31173  cdlemkid  31194  cdlemk19x  31201  cdlemk11t  31204  dihglblem5  31557  hlhilset  32196
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-nf 1545  df-nfc 2483
  Copyright terms: Public domain W3C validator