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

Theorem nfcv 2573
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 1630 . 2  |-  F/ x  y  e.  A
21nfci 2563 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   F/_wnfc 2560
This theorem is referenced by:  nfcvd  2574  nfel  2581  nfeq1  2582  nfel1  2583  nfeq2  2584  nfel2  2585  nfcvf  2595  r2al  2743  r2ex  2744  nfra2  2761  r19.12  2820  ralcom  2869  rexcom  2870  raleq  2905  rexeq  2906  reueq1  2907  rmoeq1  2908  cbvral  2929  cbvrex  2930  rabeq  2951  cbvrabv  2956  vtoclg  3012  vtocl2g  3016  vtoclga  3018  vtocl2ga  3020  vtocl3ga  3022  spcimdv  3034  spcgv  3037  spcegv  3038  rspct  3046  rspc  3047  rspce  3048  rspc2  3058  ceqsexg  3068  elabgt  3080  elabf  3082  elabg  3084  elab3g  3089  elrab  3093  mob  3117  2rmorex  3139  nfsbc1v  3181  elrabsf  3200  sbcralt  3234  sbcralg  3236  sbcrexg  3237  sbcreug  3238  cbvcsbv  3257  csbexg  3262  csbconstg  3266  nfcsb1v  3284  csbnestg  3302  cbvralcsf  3312  cbvreucsf  3314  cbvrabcsf  3315  cbvralv2  3316  cbvrexv2  3317  n0f  3637  n0  3638  raaan  3736  nfpw  3811  nfop  4001  cbviunv  4131  cbviinv  4132  ssiun2s  4136  iunab  4138  ssiinf  4141  ssiin  4142  iinab  4153  cbvdisjv  4194  disjors  4199  disji2  4200  disjprg  4209  disjxiun  4210  disjxun  4211  cbvmptv  4301  triun  4316  zfrep3cl  4328  moop2  4452  euotd  4458  opelopabf  4480  nfpo  4509  nfso  4510  pofun  4520  nffr  4557  nfse  4558  eusvnf  4719  reusv2lem4  4728  reusv2  4730  reusv6OLD  4735  rabxfrd  4745  onminesb  4779  onminsb  4780  tfis  4835  tfisi  4839  opeliunxp  4930  nfrel  4963  opeliunxp2  5014  ralxpf  5020  nfco  5039  nfcnv  5052  dfdmf  5065  dfrnf  5109  nfdm  5112  nfres  5149  dffun6f  5469  dffun6  5470  nffun  5477  nffv  5736  nffvmpt1  5737  dffn5f  5782  funfv2f  5793  fvmpts  5808  fvmpt2i  5812  fvmptss  5814  fvmptex  5816  fvmptdv  5818  fvmptnf  5823  fvmptn  5824  eqfnfv2f  5832  ralrnmpt  5879  f1ompt  5892  ffnfvf  5896  fmptco  5902  fmptcof  5903  fmptcos  5904  zfrep6  5969  abrexex2g  5989  funiunfvf  5997  abrexex2  6002  dff13f  6007  f1mpt  6008  fliftfuns  6037  nfiso  6045  mpt2eq123  6134  cbvmpt2x  6151  cbvmpt2  6152  cbvmpt2v  6153  ovmpt2s  6198  ov2gf  6199  ovmpt2dxf  6200  ovmpt2dx  6201  ovmpt2dv  6207  ovmpt2dv2  6208  ov3  6211  nfof  6311  nfofr  6312  offval2  6323  ofrfval2  6324  dfopab2  6402  dfoprab3s  6403  mpt2mptsx  6415  dmmpt2ssx  6417  fmpt2x  6418  ovmptss  6429  fmpt2co  6431  dfmpt2  6438  mpt2xopoveq  6471  mpt2xopovel  6472  nftpos  6515  tposoprab  6516  fvopab5  6535  nfriota1  6558  csbriotag  6563  riota2  6573  riotaxfrd  6582  riotasvd  6593  riotasvdOLD  6594  riotasv2d  6595  riotasv2dOLD  6596  riotasv2s  6597  riotasv3dOLD  6600  nfrecs  6636  nfrdg  6673  rdgsucmpt2  6689  rdgsucmpt  6690  frsucmpt  6696  frsucmptn  6697  frsucmpt2  6698  oawordeulem  6798  nnawordex  6881  eqerlem  6938  qliftfuns  6992  cbvixpv  7081  nfixp  7082  nfixp1  7083  ixpf  7085  mptelixpg  7100  dom2lem  7148  xpcomco  7199  xpf1o  7270  mapxpen  7274  ac6sfi  7352  iunfi  7395  indexfi  7415  dffi3  7437  nfoi  7484  ixpiunwdom  7560  cnfcomlem  7657  r1val1  7713  rankidb  7727  rankval4  7794  scottex  7810  scottexs  7812  scott0s  7813  cp  7816  tskwe  7838  cardmin2  7886  fseqenlem1  7906  dfac8clem  7914  cardaleph  7971  hsmexlem2  8308  axcc2  8318  ac6num  8360  ac6c4  8362  axdclem  8400  iundom2g  8416  uniimadomf  8421  cardmin  8440  pwfseqlem2  8535  pwfseqlem4a  8537  pwfseqlem4  8538  inar1  8651  lble  9961  nnwof  10544  nnwos  10545  fzrevral  11132  nfseq  11334  seqof2  11382  nfwrd  11741  rlim2  12291  ello1mpt  12316  rlimcld2  12373  o1compt  12382  sumeq1  12484  nfsum1  12485  nfsum  12486  sumeq2w  12487  cbvsum  12490  cbvsumv  12491  cbvsumi  12492  sumfc  12504  summolem2a  12510  zsum  12513  fsum  12515  sumss  12519  sumss2  12521  fsumcvg2  12522  fsumadd  12533  sumsn  12535  sumsns  12537  fsum2dlem  12555  fsumcnv  12558  fsumcom2  12559  fsumshftm  12565  fsum0diag2  12567  fsummulc2  12568  fsum00  12578  fsumrelem  12587  fsumrlim  12591  fsumo1  12592  o1fsum  12593  fsumiun  12601  ruclem1  12831  prmind2  13091  pcmpt  13262  pcmptdvds  13264  prdsbas3  13704  prdsdsval2  13707  mreiincl  13822  invfuc  14172  yonedalem4b  14374  odval  15173  gsum2d2lem  15548  gsum2d2  15549  gsumcom2  15550  prdsgsum  15553  dprd2d2  15603  gsumdixp  15716  lss1d  16040  psrass1lem  16443  evlslem4  16565  neiptopnei  17197  fiuncmp  17468  iuncon  17492  2ndcdisj  17520  elptr2  17607  ptbasfi  17614  ptunimpt  17628  ptcldmpt  17647  ptclsg  17648  ptcnplem  17654  ptcnp  17655  cnmpt11  17696  cnmpt1t  17698  cnmpt21  17704  cnmpt2t  17706  cnmptcom  17711  cnmptk2  17719  cnmpt2k  17721  imasnopn  17723  imasncld  17724  imasncls  17725  xkocnv  17847  elmptrab  17860  flfcnp2  18040  ptcmpg  18089  cnextfvval  18097  fmucnd  18323  prdsdsf  18398  prdsxmet  18400  cfilucfilOLD  18600  cfilucfil  18601  blval2  18606  restmetu  18618  fsumcn  18901  fsum2cn  18902  ovolfiniun  19398  ovoliunlem3  19401  ovoliun  19402  ovoliun2  19403  ovoliunnul  19404  finiunmbl  19439  volfiniun  19442  iundisj  19443  iundisj2  19444  iunmbl  19448  voliun  19449  iunmbl2  19452  mbfpos  19544  mbfposr  19545  mbfposb  19546  mbfsup  19557  mbfinf  19558  mbflim  19561  i1fposd  19600  itg1climres  19607  itg2splitlem  19641  itg2split  19642  itg2cnlem1  19654  isibl  19658  isibl2  19659  dfitg  19662  itgeq1  19665  nfitg1  19666  nfitg  19667  cbvitg  19668  cbvitgv  19669  itgmpt  19675  itgss3  19707  itgfsum  19719  itgabs  19727  itggt0  19734  itgcn  19735  cbvditgv  19743  limcmpt  19771  limciun  19782  dvmptfsum  19860  dvlipcn  19879  lhop2  19900  dvfsumle  19906  dvfsumabs  19908  dvfsumlem1  19911  dvfsumlem2  19912  dvfsumlem4  19914  dvfsumrlim  19916  dvfsum2  19919  itgparts  19932  itgsubstlem  19933  itgsubst  19934  mpfrcl  19940  elplyd  20122  coeeq2  20162  dgrle  20163  ulmss  20314  itgulm2  20326  leibpi  20783  rlimcnp  20805  rlimcnp2  20806  o1cxp  20814  fsumdvdscom  20971  fsumdvdsmul  20981  fsumvma  20998  lgseisenlem2  21135  dchrisumlema  21183  dchrisumlem2  21185  dchrisumlem3  21186  cnlnadjlem5  23575  chirred  23899  ralcom4f  23966  rexcom4f  23967  rmo4fOLD  23984  disji2f  24020  disjorsf  24023  disjif2  24024  disjabrex  24025  disjabrexf  24026  disjxpin  24029  iundisjf  24030  iundisj2f  24031  dfrel4  24035  dfimafnf  24044  suppss2f  24050  fmptdF  24070  resmptf  24072  fvmpt2f  24073  feqmptdf  24076  fmptcof2  24077  fcomptf  24078  offval2f  24081  ofpreima  24082  funcnvmptOLD  24083  funcnvmpt  24084  funcnv5mpt  24085  funcnv4mpt  24086  xrofsup  24127  iundisjfi  24153  iundisj2fi  24154  iundisjcnt  24155  iundisj2cnt  24156  gsumconstf  24223  xrge0tmd  24333  qqhval2  24367  esumcl  24428  nfesum1  24438  cbvesumv  24440  esumid  24441  esumval  24442  esumel  24443  esumnul  24444  esumsplit  24448  esumadd  24449  esumle  24450  esummono  24451  gsumesum  24452  esumlub  24453  esumaddf  24454  esumpr  24458  esumfzf  24460  esumfsup  24461  esumss  24463  esumpinfval  24464  esumpfinvalf  24467  esumpinfsum  24468  esumpcvgval  24469  esumpmono  24470  esumcocn  24471  esummulc1  24472  esummulc2  24473  esumdivc  24474  esumcvg  24477  sigaclcu2  24504  measvunilem  24567  measvunilem0  24568  measvuni  24569  measiuns  24572  measiun  24573  meascnbl  24574  voliune  24586  volfiniune  24587  volmeas  24588  imambfm  24613  sibfof  24655  lgamgulmlem2  24815  lgamgulmlem6  24819  lgamgulm2  24821  cvmcov  24951  relexpsucr  25131  prodeq1  25236  nfcprod1  25237  nfcprod  25238  prodeq2w  25239  cbvprod  25242  cbvprodv  25243  cbvprodi  25244  prodmolem2a  25261  zprod  25264  fprod  25268  fprodntriv  25269  prodfc  25272  prodss  25274  fprodmul  25285  fproddiv  25286  prodsn  25287  fprodm1s  25294  fprodp1s  25295  prodsns  25296  fprodefsum  25299  fprodn0  25304  fprod2dlem  25305  fprodcnv  25308  fprodcom2  25309  setinds  25406  dfon2lem3  25413  tfisg  25480  wfisg  25485  trpredlem1  25506  trpredtr  25509  trpredmintr  25510  trpred0  25515  trpredrec  25517  frinsg  25521  nfwrecs  25534  nfwlim  25574  sltval2  25612  nobndlem5  25652  bpolyval  26096  mbfposadd  26255  itgabsnc  26275  itggt0cn  26278  ftc1cnnclem  26279  ftc1anclem5  26285  ftc2nc  26290  finminlem  26322  indexa  26436  indexdom  26437  filbcmb  26443  sdclem2  26447  sdclem1  26448  fdc1  26451  totbndbnd  26499  heibor1  26520  elrfirn2  26751  ofmpteq  26777  mzpsubst  26806  eq0rabdioph  26836  sbccomieg  26850  rexrabdioph  26855  rexfrabdioph  26856  rabdiophlem2  26863  elnn0rabdioph  26864  dvdsrabdioph  26871  rabrenfdioph  26876  fphpd  26878  monotuz  27005  monotoddzz  27007  oddcomabszz  27008  setindtrs  27097  wdom2d2  27107  fnwe2val  27125  fnwe2lem1  27126  aomclem6  27135  aomclem8  27137  mamufval  27421  compab  27621  evth2f  27663  elunif  27664  fvelrnbf  27666  rfcnpre1  27667  fsumcnf  27669  sumsnd  27674  evthf  27675  refsumcn  27678  rfcnpre2  27679  rfcnpre3  27681  rfcnpre4  27682  rfcnnnub  27684  refsum2cnlem1  27685  refsum2cn  27686  fmul01  27687  fmuldfeqlem1  27689  fmuldfeq  27690  fmul01lt1lem1  27691  fmul01lt1lem2  27692  fmul01lt1  27693  cncfmptss  27694  mulc1cncfg  27698  infrglb  27699  expcnfg  27703  climmulf  27707  climexp  27708  climsuse  27711  climrecf  27712  climinff  27714  dvcosre  27718  itgsin0pilem1  27721  ibliccsinexp  27722  itgsinexplem1  27725  itgsinexp  27726  stoweidlem3  27729  stoweidlem14  27740  stoweidlem16  27742  stoweidlem18  27744  stoweidlem21  27747  stoweidlem23  27749  stoweidlem26  27752  stoweidlem27  27753  stoweidlem28  27754  stoweidlem29  27755  stoweidlem31  27757  stoweidlem34  27760  stoweidlem35  27761  stoweidlem36  27762  stoweidlem41  27767  stoweidlem42  27768  stoweidlem43  27769  stoweidlem46  27772  stoweidlem47  27773  stoweidlem48  27774  stoweidlem51  27777  stoweidlem52  27778  stoweidlem53  27779  stoweidlem54  27780  stoweidlem55  27781  stoweidlem56  27782  stoweidlem57  27783  stoweidlem58  27784  stoweidlem59  27785  stoweidlem60  27786  stoweidlem62  27788  stowei  27790  wallispilem5  27795  stirlinglem4  27803  stirlinglem5  27804  stirlinglem11  27810  stirlinglem12  27811  stirlinglem13  27812  stirlinglem14  27813  stirlinglem15  27814  stirling  27815  cbvral2  27927  cbvrex2  27928  raaan2  27930  2reurex  27936  2reu3  27943  2reu7  27946  2reu8  27947  eu2ndop1stv  27957  nfafv  27977  opelopabgf  28072  oprabv  28086  iunconlem2  29048  bnj23  29084  bnj1366  29202  bnj1400  29208  bnj1534  29225  bnj1542  29229  bnj607  29288  bnj873  29296  bnj958  29312  bnj1000  29313  bnj981  29322  bnj1014  29332  bnj1123  29356  bnj1204  29382  bnj1388  29403  bnj1398  29404  bnj1408  29406  bnj1445  29414  bnj1446  29415  bnj1447  29416  bnj1448  29417  bnj1449  29418  bnj1466  29423  bnj1467  29424  bnj1463  29425  bnj1312  29428  bnj1498  29431  bnj1519  29435  bnj1520  29436  bnj1525  29439  bnj1529  29440  riotaocN  30008  cdleme26ee  31158  cdleme31sn1  31179  cdleme31se2  31181  cdlemefrs29bpre0  31194  cdlemefs32sn1aw  31212  cdleme43fsv1snlem  31218  cdleme41sn3a  31231  cdleme32d  31242  cdleme32f  31244  cdleme40m  31265  cdleme40n  31266  cdleme42b  31276  ltrniotaval  31379  cdlemksv2  31645  cdlemkuv2  31665  cdlemk36  31711  cdlemk38  31713  cdlemkid  31734  cdlemk19x  31741  cdlemk11t  31744  dihglblem5  32097  hlhilset  32736
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-17 1627
This theorem depends on definitions:  df-bi 179  df-nf 1555  df-nfc 2562
  Copyright terms: Public domain W3C validator