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

Theorem nfcv 2574
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 1673 . 2  |-  F/ x  y  e.  A
21nfci 2564 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   F/_wnfc 2561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-5 1670
This theorem depends on definitions:  df-bi 185  df-nf 1590  df-nfc 2563
This theorem is referenced by:  nfcvd  2575  nfel  2582  nfeq1  2583  nfel1  2584  nfeq2  2585  nfel2  2586  nfcvf  2596  r2al  2747  r2ex  2748  nfra2  2765  r19.12  2825  ralcom  2876  rexcom  2877  raleq  2912  rexeq  2913  reueq1  2914  rmoeq1  2915  cbvral  2938  cbvrex  2939  rabeq  2961  cbvrabv  2966  vtocl2g  3029  vtoclga  3031  vtocl2ga  3033  vtocl3ga  3035  spcimdv  3049  spcgv  3052  spcegv  3053  rspct  3061  rspc  3062  rspce  3063  rspc2  3073  elabgt  3098  elabf  3100  elabg  3102  elab3g  3107  elrab  3112  2rmorex  3158  nfsbc1v  3201  elrabsf  3220  sbcralt  3262  sbcralg  3265  sbcrex  3266  sbcrexgOLD  3267  sbcreu  3268  sbcreugOLD  3269  cbvcsbv  3289  csbconstg  3296  nfcsb1v  3299  cbvralcsf  3314  cbvreucsf  3316  cbvrabcsf  3317  cbvralv2  3318  cbvrexv2  3319  n0f  3640  n0  3641  csbnestg  3689  raaan  3782  nfpw  3867  nfop  4070  cbviunv  4204  cbviinv  4205  ssiun2s  4209  iunab  4211  ssiinf  4214  ssiin  4215  iinab  4226  cbvdisjv  4268  disjors  4273  disji2  4274  disjprg  4283  disjxiun  4284  disjxun  4285  cbvmptv  4378  triun  4393  zfrep3cl  4405  csbexg  4419  csbexgOLD  4421  eusvnf  4482  reusv2lem4  4491  reusv2  4493  reusv6OLD  4498  rabxfrd  4508  moop2  4581  euotd  4587  opelopabf  4608  nfpo  4641  nfso  4642  pofun  4652  nffr  4689  nfse  4690  opeliunxp  4885  nfrel  4920  ralxpf  4981  nfco  5000  nfcnv  5013  dfdmf  5028  dfrnf  5073  nfdm  5076  nfres  5107  dffun6f  5427  dffun6  5428  nffun  5435  nffv  5693  nffvmpt1  5694  dffn5f  5741  funfv2f  5755  fvmpts  5771  fvmpt2i  5775  fvmptss  5777  fvmptex  5779  fvmptdv  5781  fvmptnf  5786  fvmptn  5787  fvopab5  5790  eqfnfv2f  5796  ralrnmpt  5847  f1ompt  5860  ffnfvf  5865  fmptco  5871  fmptcof  5872  fmptcos  5873  funiunfvf  5961  dff13f  5968  f1mpt  5969  fliftfuns  6002  nfiso  6010  csbriota  6059  riota2  6070  riotaxfrd  6078  mpt2eq123  6140  cbvmpt2x  6159  cbvmpt2  6160  cbvmpt2v  6161  ovmpt2s  6209  ov2gf  6210  ovmpt2dxf  6211  ovmpt2dx  6212  ovmpt2dv  6218  ovmpt2dv2  6219  ov3  6222  nfof  6320  nfofr  6321  offval2  6331  ofrfval2  6332  ofmpteq  6333  onminesb  6404  onminsb  6405  tfis  6460  tfisi  6464  zfrep6  6540  abrexex2g  6549  abrexex2  6553  dfopab2  6623  dfoprab3s  6624  mpt2mptsx  6632  dmmpt2ssx  6634  fmpt2x  6635  fnmpt2ovd  6646  offval22  6647  ovmptss  6649  fmpt2co  6651  dfmpt2  6658  mpt2xopoveq  6731  mpt2xopovel  6732  nftpos  6775  tposoprab  6776  nfrecs  6826  nfrdg  6862  rdgsucmpt2  6878  rdgsucmpt  6879  frsucmpt  6885  frsucmptn  6886  frsucmpt2  6887  oawordeulem  6985  nnawordex  7068  eqerlem  7125  qliftfuns  7179  cbvixpv  7273  nfixp  7274  nfixp1  7275  ixpf  7277  mptelixpg  7292  dom2lem  7341  xpcomco  7393  xpf1o  7465  mapxpen  7469  ac6sfi  7548  iunfi  7591  indexfi  7611  dffi3  7673  nfoi  7720  ixpiunwdom  7798  cantnflem1  7889  cnfcomlem  7924  cnfcomlemOLD  7932  r1val1  7985  rankidb  7999  rankval4  8066  scottex  8084  scottexs  8086  scott0s  8087  cp  8090  tskwe  8112  cardmin2  8160  fseqenlem1  8186  dfac8clem  8194  cardaleph  8251  hsmexlem2  8588  axcc2  8598  ac6num  8640  ac6c4  8642  axdclem  8680  iundom2g  8696  uniimadomf  8701  cardmin  8720  pwfseqlem2  8818  pwfseqlem4a  8820  pwfseqlem4  8821  inar1  8934  lble  10274  nnwof  10913  nnwos  10914  fzrevral  11536  nfseq  11808  seqof2  11856  nfwrd  12248  rlim2  12966  ello1mpt  12991  rlimcld2  13048  o1compt  13057  nfsum1  13159  nfsum  13160  sumeq2w  13161  sumeq2ii  13162  cbvsumv  13165  cbvsumi  13166  sumfc  13178  summolem2a  13184  zsum  13187  fsum  13189  sumss  13193  sumss2  13195  fsumcvg2  13196  fsumadd  13207  sumsn  13209  sumsns  13211  fsum2dlem  13229  fsumcnv  13232  fsumcom2  13233  fsumshftm  13240  fsum0diag2  13242  fsummulc2  13243  fsum00  13253  fsumrelem  13262  fsumrlim  13266  fsumo1  13267  o1fsum  13268  fsumiun  13276  ruclem1  13505  prmind2  13766  pcmpt  13946  pcmptdvds  13948  prdsbas3  14411  prdsdsval2  14414  mreiincl  14526  invfuc  14876  yonedalem4b  15078  odval  16028  gsumconstf  16418  gsummptshft  16419  gsummpt1n0  16446  gsum2d2lem  16455  gsum2d2  16456  gsumcom2  16457  prdsgsum  16461  prdsgsumOLD  16462  dprd2d2  16533  gsumdixpOLD  16690  gsumdixp  16691  lss1d  17024  psrass1lem  17427  evlslem4OLD  17570  evlslem4  17571  mpfrcl  17584  evl1gsumdlem  17770  mamufval  18263  mdetralt2  18395  mdetunilem2  18399  madugsum  18429  gsummatr01lem4  18444  neiptopnei  18716  fiuncmp  18987  iuncon  19012  2ndcdisj  19040  elptr2  19127  ptbasfi  19134  ptunimpt  19148  ptcldmpt  19167  ptclsg  19168  ptcnplem  19174  ptcnp  19175  cnmpt11  19216  cnmpt1t  19218  cnmpt21  19224  cnmpt2t  19226  cnmptcom  19231  cnmptk2  19239  cnmpt2k  19241  imasnopn  19243  imasncld  19244  imasncls  19245  xkocnv  19367  elmptrab  19380  flfcnp2  19560  ptcmpg  19609  fmucnd  19847  prdsdsf  19922  prdsxmet  19924  cfilucfilOLD  20124  cfilucfil  20125  blval2  20130  restmetu  20142  fsumcn  20426  fsum2cn  20427  ovolfiniun  20964  ovoliunlem3  20967  ovoliun  20968  ovoliun2  20969  ovoliunnul  20970  finiunmbl  21005  volfiniun  21008  iundisj  21009  iundisj2  21010  iunmbl  21014  voliun  21015  iunmbl2  21018  mbfpos  21109  mbfposr  21110  mbfposb  21111  mbfsup  21122  mbfinf  21123  mbflim  21126  i1fposd  21165  itg1climres  21172  itg2splitlem  21206  itg2split  21207  itg2cnlem1  21219  isibl  21223  isibl2  21224  dfitg  21227  itgeq1  21230  nfitg1  21231  nfitg  21232  cbvitg  21233  cbvitgv  21234  itgmpt  21240  itgss3  21272  itgfsum  21284  itgabs  21292  itggt0  21299  itgcn  21300  cbvditgv  21310  limcmpt  21338  limciun  21349  dvmptfsum  21427  dvlipcn  21446  lhop2  21467  dvfsumle  21473  dvfsumabs  21475  dvfsumlem1  21478  dvfsumlem2  21479  dvfsumlem4  21481  dvfsumrlim  21483  dvfsum2  21486  itgparts  21499  itgsubstlem  21500  itgsubst  21501  elplyd  21650  coeeq2  21690  dgrle  21691  ulmss  21842  itgulm2  21854  leibpi  22317  rlimcnp  22339  rlimcnp2  22340  o1cxp  22348  fsumdvdscom  22505  fsumdvdsmul  22515  fsumvma  22532  lgseisenlem2  22669  dchrisumlema  22717  dchrisumlem2  22719  dchrisumlem3  22720  cnlnadjlem5  25443  chirred  25767  ralcom4f  25828  rexcom4f  25829  rmo4fOLD  25848  disji2f  25889  disjorsf  25892  disjif2  25893  disjabrex  25894  disjabrexf  25895  disjxpin  25898  iundisjf  25899  iundisj2f  25900  disjunsn  25904  dfrel4  25905  opabdm  25911  opabrn  25912  ssrelf  25913  dfimafnf  25918  suppss2f  25922  fmptdF  25940  resmptf  25942  fvmpt2f  25943  feqmptdf  25946  fmptcof2  25947  fcomptf  25948  offval2f  25951  ofpreima  25952  funcnvmptOLD  25954  funcnvmpt  25955  funcnv5mpt  25956  funcnv4mpt  25957  mpt2mptxf  25963  f1od2  25992  fcobijfs  25994  fpwrelmap  26001  fpwrelmapffs  26002  xrofsup  26023  iundisjfi  26048  iundisj2fi  26049  iundisjcnt  26050  iundisj2cnt  26051  nnindf  26057  gsummpt2co  26217  gsumvsca1  26219  gsumvsca2  26220  ordtconlem1  26323  xrge0tmd  26345  qqhval2  26380  esumcl  26455  nfesum1  26465  cbvesumv  26467  esumid  26468  esumval  26469  esumel  26470  esumnul  26471  esumsplit  26475  esumadd  26476  esumle  26477  esummono  26478  gsumesum  26479  esumlub  26480  esumaddf  26481  esumpr  26485  esumfzf  26487  esumfsup  26488  esumss  26490  esumpinfval  26491  esumpfinvalf  26494  esumpinfsum  26495  esumpcvgval  26496  esumpmono  26497  esumcocn  26498  esummulc1  26499  esummulc2  26500  esumdivc  26501  esumcvg  26504  sigaclcu2  26532  measvunilem  26595  measvunilem0  26596  measvuni  26597  measiuns  26600  measiun  26601  meascnbl  26602  voliune  26614  volfiniune  26615  volmeas  26616  ddemeas  26621  imambfm  26646  oms0  26679  omsmon  26680  sibfof  26695  eulerpartlemn  26733  eulerpart  26734  lgamgulmlem2  26985  lgamgulmlem6  26989  lgamgulm2  26991  cvmcov  27121  relexpsucr  27301  prodeq1  27391  nfcprod1  27392  nfcprod  27393  prodeq2w  27394  cbvprod  27397  cbvprodv  27398  cbvprodi  27399  prodmolem2a  27416  zprod  27419  fprod  27423  fprodntriv  27424  prodfc  27427  prodss  27429  fprodmul  27440  fproddiv  27441  prodsn  27442  fprodm1s  27449  fprodp1s  27450  prodsns  27451  fprodefsum  27454  fprodn0  27459  fprod2dlem  27460  fprodcnv  27463  fprodcom2  27464  setinds  27560  dfon2lem3  27567  tfisg  27634  wfisg  27639  trpredlem1  27660  trpredtr  27663  trpredmintr  27664  trpred0  27669  trpredrec  27671  frinsg  27675  nfwrecs  27688  nfwlim  27728  sltval2  27766  nobndlem5  27806  bpolyval  28161  finixpnum  28385  ptrest  28396  mbfposadd  28410  dvtanlem  28412  itgabsnc  28432  itggt0cn  28435  ftc1cnnclem  28436  ftc1anclem5  28442  ftc2nc  28447  finminlem  28484  indexa  28598  indexdom  28599  filbcmb  28605  sdclem2  28609  sdclem1  28610  fdc1  28613  totbndbnd  28659  heibor1  28680  scottexf  28951  scott0f  28952  ac6s6f  28956  elrfirn2  29003  mzpsubst  29056  eq0rabdioph  29086  sbccomieg  29102  rexrabdioph  29103  rexfrabdioph  29104  rabdiophlem2  29111  elnn0rabdioph  29112  dvdsrabdioph  29119  rabrenfdioph  29124  fphpd  29126  monotuz  29253  monotoddzz  29255  oddcomabszz  29256  setindtrs  29345  wdom2d2  29355  fnwe2val  29373  fnwe2lem1  29374  aomclem6  29383  aomclem8  29385  areaquad  29563  compab  29668  evth2f  29708  elunif  29709  fvelrnbf  29711  rfcnpre1  29712  fsumcnf  29714  sumsnd  29719  evthf  29720  refsumcn  29723  rfcnpre2  29724  rfcnpre3  29726  rfcnpre4  29727  rfcnnnub  29729  refsum2cnlem1  29730  refsum2cn  29731  fmul01  29732  fmuldfeqlem1  29734  fmuldfeq  29735  fmul01lt1lem1  29736  fmul01lt1lem2  29737  fmul01lt1  29738  cncfmptss  29739  mulc1cncfg  29741  infrglb  29742  expcnfg  29744  climmulf  29748  climexp  29749  climsuse  29752  climrecf  29753  climinff  29755  dvcosre  29759  itgsin0pilem1  29761  ibliccsinexp  29762  itgsinexplem1  29765  itgsinexp  29766  stoweidlem3  29769  stoweidlem14  29780  stoweidlem16  29782  stoweidlem18  29784  stoweidlem21  29787  stoweidlem23  29789  stoweidlem26  29792  stoweidlem27  29793  stoweidlem28  29794  stoweidlem29  29795  stoweidlem31  29797  stoweidlem34  29800  stoweidlem35  29801  stoweidlem36  29802  stoweidlem41  29807  stoweidlem42  29808  stoweidlem43  29809  stoweidlem46  29812  stoweidlem47  29813  stoweidlem48  29814  stoweidlem51  29817  stoweidlem52  29818  stoweidlem53  29819  stoweidlem54  29820  stoweidlem55  29821  stoweidlem56  29822  stoweidlem57  29823  stoweidlem58  29824  stoweidlem59  29825  stoweidlem60  29826  stoweidlem62  29828  stowei  29830  wallispilem5  29835  stirlinglem4  29843  stirlinglem5  29844  stirlinglem11  29850  stirlinglem12  29851  stirlinglem13  29852  stirlinglem14  29853  stirlinglem15  29854  stirling  29855  cbvral2  29967  cbvrex2  29968  raaan2  29970  2reurex  29976  2reu3  29983  2reu7  29986  2reu8  29987  eu2ndop1stv  29997  nfafv  30013  opelopabgf  30107  elfvmptrab1  30125  oprabv  30128  elovmpt2rab  30129  elovmpt2rab1  30130  ovmpt3rab1  30132  ovmpt3rabdm  30133  elovmpt3rab1  30134  rabasiun  30201  hashrabsn1  30204  fsumz  30207  fsummsndifre  30208  fsumsplitsndif  30209  fsummmodsndifre  30210  fsummsnunz  30212  fsumsplitsnun  30213  fsummmodsnunre  30214  opeliun2xp  30690  dmmpt2ssx2  30697  ovmpt2rdxf  30699  ovmpt2rdx  30700  rabssnn0fi  30716  coe1fzgsumdlem  30802  gsummoncoe1  30808  iunconlem2  31600  bnj23  31636  bnj1366  31752  bnj1400  31758  bnj1534  31775  bnj1542  31779  bnj607  31838  bnj873  31846  bnj958  31862  bnj1000  31863  bnj981  31872  bnj1014  31882  bnj1123  31906  bnj1204  31932  bnj1388  31953  bnj1398  31954  bnj1408  31956  bnj1445  31964  bnj1446  31965  bnj1447  31966  bnj1448  31967  bnj1449  31968  bnj1466  31973  bnj1467  31974  bnj1463  31975  bnj1312  31978  bnj1498  31981  bnj1519  31985  bnj1520  31986  bnj1525  31989  bnj1529  31990  bj-rabtrALT  32333  riotasvd  32500  riotasv2d  32501  riotasv2s  32502  riotaocN  32747  cdleme26ee  33897  cdleme31sn1  33918  cdleme31se2  33920  cdlemefrs29bpre0  33933  cdlemefs32sn1aw  33951  cdleme43fsv1snlem  33957  cdleme41sn3a  33970  cdleme32d  33981  cdleme32f  33983  cdleme40m  34004  cdleme40n  34005  cdleme42b  34015  ltrniotaval  34118  cdlemksv2  34384  cdlemkuv2  34404  cdlemk36  34450  cdlemk38  34452  cdlemkid  34473  cdlemk19x  34480  cdlemk11t  34483  dihglblem5  34836  hlhilset  35475
  Copyright terms: Public domain W3C validator