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

Theorem nfcv 2613
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 1674 . 2  |-  F/ x  y  e.  A
21nfci 2602 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   F/_wnfc 2599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-5 1671
This theorem depends on definitions:  df-bi 185  df-nf 1591  df-nfc 2601
This theorem is referenced by:  nfcvd  2614  nfelOLD  2626  nfeq1  2627  nfel1  2628  nfeq2  2629  nfel2  2630  nfcvf  2637  r2al  2856  r2ex  2857  nfra2  2879  r19.12  2926  ralcom  2977  rexcom  2978  raleq  3013  rexeq  3014  reueq1  3015  rmoeq1  3016  cbvral  3039  cbvrex  3040  rabeq  3062  cbvrabv  3067  vtocl2g  3130  vtoclga  3132  vtocl2ga  3134  vtocl3ga  3136  spcimdv  3150  spcgv  3153  spcegv  3154  rspct  3162  rspc  3163  rspce  3164  rspc2  3175  elabgt  3200  elabf  3202  elabg  3204  elab3g  3209  elrab  3214  2rmorex  3261  nfsbc1v  3304  elrabsf  3323  sbcralt  3365  sbcralg  3368  sbcrex  3369  sbcrexgOLD  3370  sbcreu  3371  sbcreugOLD  3372  cbvcsbv  3392  csbconstg  3399  nfcsb1v  3402  cbvralcsf  3417  cbvreucsf  3419  cbvrabcsf  3420  cbvralv2  3421  cbvrexv2  3422  n0f  3743  n0  3744  csbnestg  3792  raaan  3885  nfpw  3970  nfop  4173  cbviunv  4307  cbviinv  4308  ssiun2s  4312  iunab  4314  ssiinf  4317  ssiin  4318  iinab  4329  cbvdisjv  4371  disjors  4376  disji2  4377  disjprg  4386  disjxiun  4387  disjxun  4388  cbvmptv  4481  triun  4496  zfrep3cl  4508  csbexg  4522  csbexgOLD  4524  eusvnf  4585  reusv2lem4  4594  reusv2  4596  reusv6OLD  4601  rabxfrd  4611  moop2  4684  euotd  4690  opelopabf  4711  nfpo  4744  nfso  4745  pofun  4755  nffr  4792  nfse  4793  opeliunxp  4988  nfrel  5023  ralxpf  5084  nfco  5103  nfcnv  5116  dfdmf  5131  dfrnf  5176  nfdm  5179  nfres  5210  dffun6f  5530  dffun6  5531  nffun  5538  nffv  5796  nffvmpt1  5797  dffn5f  5845  funfv2f  5859  fvmpts  5875  fvmpt2i  5879  fvmptss  5881  fvmptex  5883  fvmptdv  5885  fvmptnf  5890  fvmptn  5891  fvopab5  5894  eqfnfv2f  5900  ralrnmpt  5951  f1ompt  5964  ffnfvf  5969  fmptco  5975  fmptcof  5976  fmptcos  5977  funiunfvf  6065  dff13f  6072  f1mpt  6073  fliftfuns  6106  nfiso  6114  csbriota  6163  riota2  6174  riotaxfrd  6182  mpt2eq123  6244  cbvmpt2x  6263  cbvmpt2  6264  cbvmpt2v  6265  ovmpt2s  6314  ov2gf  6315  ovmpt2dxf  6316  ovmpt2dx  6317  ovmpt2dv  6323  ovmpt2dv2  6324  ov3  6327  nfof  6425  nfofr  6426  offval2  6436  ofrfval2  6437  ofmpteq  6438  onminesb  6509  onminsb  6510  tfis  6565  tfisi  6569  zfrep6  6645  abrexex2g  6654  abrexex2  6658  dfopab2  6728  dfoprab3s  6729  mpt2mptsx  6737  dmmpt2ssx  6739  fmpt2x  6740  fnmpt2ovd  6751  offval22  6752  ovmptss  6754  fmpt2co  6756  dfmpt2  6763  mpt2xopoveq  6836  mpt2xopovel  6837  nftpos  6880  tposoprab  6881  mpt2curryd  6888  mpt2curryvald  6889  fvmpt2curryd  6890  nfrecs  6934  nfrdg  6970  rdgsucmpt2  6986  rdgsucmpt  6987  frsucmpt  6993  frsucmptn  6994  frsucmpt2  6995  oawordeulem  7093  nnawordex  7176  eqerlem  7233  qliftfuns  7287  cbvixpv  7381  nfixp  7382  nfixp1  7383  ixpf  7385  mptelixpg  7400  dom2lem  7449  xpcomco  7501  xpf1o  7573  mapxpen  7577  ac6sfi  7657  iunfi  7700  indexfi  7720  dffi3  7782  nfoi  7829  ixpiunwdom  7907  cantnflem1  7998  cnfcomlem  8033  cnfcomlemOLD  8041  r1val1  8094  rankidb  8108  rankval4  8175  scottex  8193  scottexs  8195  scott0s  8196  cp  8199  tskwe  8221  cardmin2  8269  fseqenlem1  8295  dfac8clem  8303  cardaleph  8360  hsmexlem2  8697  axcc2  8707  ac6num  8749  ac6c4  8751  axdclem  8789  iundom2g  8805  uniimadomf  8810  cardmin  8829  pwfseqlem2  8927  pwfseqlem4a  8929  pwfseqlem4  8930  inar1  9043  lble  10383  nnwof  11022  nnwos  11023  fzrevral  11645  nfseq  11917  seqof2  11965  nfwrd  12358  rlim2  13076  ello1mpt  13101  rlimcld2  13158  o1compt  13167  nfsum1  13269  nfsum  13270  sumeq2w  13271  sumeq2ii  13272  cbvsumv  13275  cbvsumi  13276  sumfc  13288  summolem2a  13294  zsum  13297  fsum  13299  sumss  13303  sumss2  13305  fsumcvg2  13306  fsumadd  13317  sumsn  13319  sumsns  13321  fsum2dlem  13339  fsumcnv  13342  fsumcom2  13343  fsumshftm  13350  fsum0diag2  13352  fsummulc2  13353  fsum00  13363  fsumrelem  13372  fsumrlim  13376  fsumo1  13377  o1fsum  13378  fsumiun  13386  ruclem1  13615  prmind2  13876  pcmpt  14056  pcmptdvds  14058  prdsbas3  14521  prdsdsval2  14524  mreiincl  14636  invfuc  14986  yonedalem4b  15188  odval  16141  gsumconstf  16533  gsummptshft  16534  gsummpt1n0  16561  gsum2d2lem  16570  gsum2d2  16571  gsumcom2  16572  prdsgsum  16576  prdsgsumOLD  16577  dprd2d2  16648  gsumdixpOLD  16806  gsumdixp  16807  lss1d  17150  psrass1lem  17553  evlslem4OLD  17697  evlslem4  17698  mpfrcl  17711  evl1gsumdlem  17899  mamufval  18392  mdetralt2  18531  mdetunilem2  18535  madugsum  18565  gsummatr01lem4  18580  neiptopnei  18852  fiuncmp  19123  iuncon  19148  2ndcdisj  19176  elptr2  19263  ptbasfi  19270  ptunimpt  19284  ptcldmpt  19303  ptclsg  19304  ptcnplem  19310  ptcnp  19311  cnmpt11  19352  cnmpt1t  19354  cnmpt21  19360  cnmpt2t  19362  cnmptcom  19367  cnmptk2  19375  cnmpt2k  19377  imasnopn  19379  imasncld  19380  imasncls  19381  xkocnv  19503  elmptrab  19516  flfcnp2  19696  ptcmpg  19745  fmucnd  19983  prdsdsf  20058  prdsxmet  20060  cfilucfilOLD  20260  cfilucfil  20261  blval2  20266  restmetu  20278  fsumcn  20562  fsum2cn  20563  ovolfiniun  21100  ovoliunlem3  21103  ovoliun  21104  ovoliun2  21105  ovoliunnul  21106  finiunmbl  21141  volfiniun  21144  iundisj  21145  iundisj2  21146  iunmbl  21150  voliun  21151  iunmbl2  21154  mbfpos  21245  mbfposr  21246  mbfposb  21247  mbfsup  21258  mbfinf  21259  mbflim  21262  i1fposd  21301  itg1climres  21308  itg2splitlem  21342  itg2split  21343  itg2cnlem1  21355  isibl  21359  isibl2  21360  dfitg  21363  itgeq1  21366  nfitg1  21367  nfitg  21368  cbvitg  21369  cbvitgv  21370  itgmpt  21376  itgss3  21408  itgfsum  21420  itgabs  21428  itggt0  21435  itgcn  21436  cbvditgv  21446  limcmpt  21474  limciun  21485  dvmptfsum  21563  dvlipcn  21582  lhop2  21603  dvfsumle  21609  dvfsumabs  21611  dvfsumlem1  21614  dvfsumlem2  21615  dvfsumlem4  21617  dvfsumrlim  21619  dvfsum2  21622  itgparts  21635  itgsubstlem  21636  itgsubst  21637  elplyd  21786  coeeq2  21826  dgrle  21827  ulmss  21978  itgulm2  21990  leibpi  22453  rlimcnp  22475  rlimcnp2  22476  o1cxp  22484  fsumdvdscom  22641  fsumdvdsmul  22651  fsumvma  22668  lgseisenlem2  22805  dchrisumlema  22853  dchrisumlem2  22855  dchrisumlem3  22856  istrkg2ld  23038  cnlnadjlem5  25610  chirred  25934  ralcom4f  25995  rexcom4f  25996  rmo4fOLD  26015  disji2f  26055  disjorsf  26058  disjif2  26059  disjabrex  26060  disjabrexf  26061  disjxpin  26064  iundisjf  26065  iundisj2f  26066  disjunsn  26070  dfrel4  26071  opabdm  26077  opabrn  26078  ssrelf  26079  dfimafnf  26084  suppss2f  26088  fmptdF  26106  resmptf  26108  fvmpt2f  26109  feqmptdf  26112  fmptcof2  26113  fcomptf  26114  offval2f  26117  ofpreima  26118  funcnvmptOLD  26120  funcnvmpt  26121  funcnv5mpt  26122  funcnv4mpt  26123  mpt2mptxf  26129  f1od2  26158  fcobijfs  26160  fpwrelmap  26167  fpwrelmapffs  26168  xrofsup  26189  iundisjfi  26214  iundisj2fi  26215  iundisjcnt  26216  iundisj2cnt  26217  nnindf  26223  gsummpt2co  26383  gsumvsca1  26385  gsumvsca2  26386  ordtconlem1  26488  xrge0tmd  26510  qqhval2  26545  esumcl  26620  nfesum1  26630  cbvesumv  26632  esumid  26633  esumval  26634  esumel  26635  esumnul  26636  esumsplit  26640  esumadd  26641  esumle  26642  esummono  26643  gsumesum  26644  esumlub  26645  esumaddf  26646  esumpr  26650  esumfzf  26652  esumfsup  26653  esumss  26655  esumpinfval  26656  esumpfinvalf  26659  esumpinfsum  26660  esumpcvgval  26661  esumpmono  26662  esumcocn  26663  esummulc1  26664  esummulc2  26665  esumdivc  26666  esumcvg  26669  sigaclcu2  26697  measvunilem  26760  measvunilem0  26761  measvuni  26762  measiuns  26765  measiun  26766  meascnbl  26767  voliune  26779  volfiniune  26780  volmeas  26781  ddemeas  26786  imambfm  26811  oms0  26844  omsmon  26845  sibfof  26860  eulerpartlemn  26898  eulerpart  26899  lgamgulmlem2  27150  lgamgulmlem6  27154  lgamgulm2  27156  cvmcov  27286  relexpsucr  27466  prodeq1  27556  nfcprod1  27557  nfcprod  27558  prodeq2w  27559  cbvprod  27562  cbvprodv  27563  cbvprodi  27564  prodmolem2a  27581  zprod  27584  fprod  27588  fprodntriv  27589  prodfc  27592  prodss  27594  fprodmul  27605  fproddiv  27606  prodsn  27607  fprodm1s  27614  fprodp1s  27615  prodsns  27616  fprodefsum  27619  fprodn0  27624  fprod2dlem  27625  fprodcnv  27628  fprodcom2  27629  setinds  27725  dfon2lem3  27732  tfisg  27799  wfisg  27804  trpredlem1  27825  trpredtr  27828  trpredmintr  27829  trpred0  27834  trpredrec  27836  frinsg  27840  nfwrecs  27853  nfwlim  27893  sltval2  27931  nobndlem5  27971  bpolyval  28326  finixpnum  28552  ptrest  28563  mbfposadd  28577  dvtanlem  28579  itgabsnc  28599  itggt0cn  28602  ftc1cnnclem  28603  ftc1anclem5  28609  ftc2nc  28614  finminlem  28651  indexa  28765  indexdom  28766  filbcmb  28772  sdclem2  28776  sdclem1  28777  fdc1  28780  totbndbnd  28826  heibor1  28847  scottexf  29118  scott0f  29119  ac6s6f  29123  elrfirn2  29170  mzpsubst  29223  eq0rabdioph  29253  sbccomieg  29269  rexrabdioph  29270  rexfrabdioph  29271  rabdiophlem2  29278  elnn0rabdioph  29279  dvdsrabdioph  29286  rabrenfdioph  29291  fphpd  29293  monotuz  29420  monotoddzz  29422  oddcomabszz  29423  setindtrs  29512  wdom2d2  29522  fnwe2val  29540  fnwe2lem1  29541  aomclem6  29550  aomclem8  29552  areaquad  29730  compab  29835  evth2f  29875  elunif  29876  fvelrnbf  29878  rfcnpre1  29879  fsumcnf  29881  sumsnd  29886  evthf  29887  refsumcn  29890  rfcnpre2  29891  rfcnpre3  29893  rfcnpre4  29894  rfcnnnub  29896  refsum2cnlem1  29897  refsum2cn  29898  fmul01  29899  fmuldfeqlem1  29901  fmuldfeq  29902  fmul01lt1lem1  29903  fmul01lt1lem2  29904  fmul01lt1  29905  cncfmptss  29906  mulc1cncfg  29908  infrglb  29909  expcnfg  29911  climmulf  29915  climexp  29916  climsuse  29919  climrecf  29920  climinff  29922  dvcosre  29926  itgsin0pilem1  29928  ibliccsinexp  29929  itgsinexplem1  29932  itgsinexp  29933  stoweidlem3  29936  stoweidlem14  29947  stoweidlem16  29949  stoweidlem18  29951  stoweidlem21  29954  stoweidlem23  29956  stoweidlem26  29959  stoweidlem27  29960  stoweidlem28  29961  stoweidlem29  29962  stoweidlem31  29964  stoweidlem34  29967  stoweidlem35  29968  stoweidlem36  29969  stoweidlem41  29974  stoweidlem42  29975  stoweidlem43  29976  stoweidlem46  29979  stoweidlem47  29980  stoweidlem48  29981  stoweidlem51  29984  stoweidlem52  29985  stoweidlem53  29986  stoweidlem54  29987  stoweidlem55  29988  stoweidlem56  29989  stoweidlem57  29990  stoweidlem58  29991  stoweidlem59  29992  stoweidlem60  29993  stoweidlem62  29995  stowei  29997  wallispilem5  30002  stirlinglem4  30010  stirlinglem5  30011  stirlinglem11  30017  stirlinglem12  30018  stirlinglem13  30019  stirlinglem14  30020  stirlinglem15  30021  stirling  30022  cbvral2  30134  cbvrex2  30135  raaan2  30137  2reurex  30143  2reu3  30150  2reu7  30153  2reu8  30154  eu2ndop1stv  30164  nfafv  30180  opelopabgf  30274  elfvmptrab1  30292  oprabv  30295  elovmpt2rab  30296  elovmpt2rab1  30297  ovmpt3rab1  30299  ovmpt3rabdm  30300  elovmpt3rab1  30301  rabasiun  30368  hashrabsn1  30371  fsumz  30374  fsummsndifre  30375  fsumsplitsndif  30376  fsummmodsndifre  30377  fsummsnunz  30379  fsumsplitsnun  30380  fsummmodsnunre  30381  opeliun2xp  30858  dmmpt2ssx2  30865  ovmpt2rdxf  30867  ovmpt2rdx  30868  rabssnn0fi  30885  coe1fzgsumdlem  30979  gsummoncoe1  30985  gsumply1eq  30994  cayleyhamilton1  31347  iunconlem2  31971  bnj23  32007  bnj1366  32123  bnj1400  32129  bnj1534  32146  bnj1542  32150  bnj607  32209  bnj873  32217  bnj958  32233  bnj1000  32234  bnj981  32243  bnj1014  32253  bnj1123  32277  bnj1204  32303  bnj1388  32324  bnj1398  32325  bnj1408  32327  bnj1445  32335  bnj1446  32336  bnj1447  32337  bnj1448  32338  bnj1449  32339  bnj1466  32344  bnj1467  32345  bnj1463  32346  bnj1312  32349  bnj1498  32352  bnj1519  32356  bnj1520  32357  bnj1525  32360  bnj1529  32361  bj-rabtrALT  32733  fsumshftd  32908  fsumshftdOLD  32909  riotasvd  32913  riotasv2d  32914  riotasv2s  32915  riotaocN  33160  cdleme26ee  34310  cdleme31sn1  34331  cdleme31se2  34333  cdlemefrs29bpre0  34346  cdlemefs32sn1aw  34364  cdleme43fsv1snlem  34370  cdleme41sn3a  34383  cdleme32d  34394  cdleme32f  34396  cdleme40m  34417  cdleme40n  34418  cdleme42b  34428  ltrniotaval  34531  cdlemksv2  34797  cdlemkuv2  34817  cdlemk36  34863  cdlemk38  34865  cdlemkid  34886  cdlemk19x  34893  cdlemk11t  34896  dihglblem5  35249  hlhilset  35888
  Copyright terms: Public domain W3C validator