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

Theorem nfcv 2603
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 1772 . 2  |-  F/ x  y  e.  A
21nfci 2593 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1898   F/_wnfc 2590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-5 1769
This theorem depends on definitions:  df-bi 190  df-nf 1679  df-nfc 2592
This theorem is referenced by:  nfcvd  2604  nfeq1  2616  nfel1  2617  nfeq2  2618  nfel2  2619  nfcvf  2626  r2alOLD  2779  nfra2  2787  r2exOLD  2926  r19.12  2928  ralcom  2963  rexcom  2964  raleq  2999  rexeq  3000  reueq1  3001  rmoeq1  3002  cbvral  3027  cbvrex  3028  rabeq  3050  cbvrabv  3056  vtocl2g  3123  vtoclga  3125  vtocl2ga  3127  vtocl3ga  3129  spcimdv  3143  spcgv  3146  spcegv  3147  rspct  3155  rspc  3156  rspce  3157  rspc2  3170  elabgt  3194  elabf  3196  elabg  3198  elab3g  3203  elrab  3208  2rmorex  3256  nfsbc1v  3299  elrabsf  3318  sbcralt  3352  sbcralg  3354  sbcrex  3355  sbcreu  3356  cbvcsbv  3381  csbconstg  3388  nfcsb1v  3391  csbie  3401  cbvralcsf  3407  cbvreucsf  3409  cbvrabcsf  3410  cbvralv2  3411  cbvrexv2  3412  n0f  3752  n0  3753  csbnestg  3799  raaan  3889  nfpw  3975  nfop  4196  rabasiun  4296  cbviunv  4331  cbviinv  4332  ssiun2s  4336  iunab  4338  ssiinf  4341  ssiin  4342  iinab  4353  iunxdif3  4378  cbvdisjv  4400  disjors  4404  disji2  4405  invdisjrab  4408  disjprg  4414  disjxiun  4415  disjxun  4416  cbvmptv  4511  triun  4526  zfrep3cl  4538  csbexg  4553  eusvnf  4615  reusv2lem4  4624  reusv2  4626  rabxfrd  4638  moop2  4713  euotd  4719  opelopabgf  4738  opelopabf  4743  nfpo  4782  nfso  4783  pofun  4793  nffr  4830  nfse  4831  opeliunxp  4908  nfrel  4942  ralxpf  5003  nfco  5022  nfcnv  5035  dfdmf  5050  dfrnf  5095  nfdm  5098  nfres  5129  dfrel4  5310  wfisg  5438  dffun6f  5619  dffun6  5620  nffun  5627  nffv  5899  nffvmpt1  5900  feqmptdf  5947  dffn5f  5948  funfv2f  5962  fvmpt2f  5977  fvmpts  5979  fvmpt2i  5984  fvmptss  5986  fvmptex  5988  fvmptdv  5990  fvmptnf  5995  fvmptn  5996  elfvmptrab1  5998  fvopab5  6002  eqfnfv2f  6008  ralrnmpt  6059  f1ompt  6072  ffnfvf  6078  fmptco  6085  fmptcof  6086  fmptcos  6087  funiunfvf  6184  dff13f  6190  f1mpt  6192  fliftfuns  6237  nfiso  6245  csbriota  6294  riota2  6304  riotaxfrd  6312  oprabv  6371  mpt2eq123  6382  cbvmpt2x  6401  cbvmpt2  6402  cbvmpt2v  6403  ovmpt2s  6452  ov2gf  6453  ovmpt2dxf  6454  ovmpt2dx  6455  ovmpt2dv  6461  ovmpt2dv2  6462  ov3  6465  elovmpt2rab  6547  elovmpt2rab1  6548  ovmpt3rab1  6557  ovmpt3rabdm  6558  elovmpt3rab1  6559  nfof  6568  nfofr  6569  offval2f  6575  offval2  6580  ofrfval2  6581  ofmpteq  6582  onminesb  6657  onminsb  6658  tfis  6713  tfisi  6717  zfrep6  6793  abrexex2g  6802  abrexex2  6806  dfopab2  6879  dfoprab3s  6880  mpt2mptsx  6888  dmmpt2ssx  6890  fmpt2x  6891  fnmpt2ovd  6903  offval22  6904  ovmptss  6909  fmpt2co  6911  dfmpt2  6918  mpt2xopoveq  6997  mpt2xopovel  6998  nftpos  7039  tposoprab  7040  mpt2curryd  7047  mpt2curryvald  7048  fvmpt2curryd  7049  nfwrecs  7061  nfrecs  7124  nfrdg  7163  rdgsucmpt2  7179  rdgsucmpt  7180  frsucmpt  7186  frsucmptn  7187  frsucmpt2  7188  oawordeulem  7286  nnawordex  7369  qliftfuns  7481  cbvixpv  7571  nfixp  7572  nfixp1  7573  ixpf  7575  mptelixpg  7590  dom2lem  7640  xpcomco  7693  xpf1o  7765  mapxpen  7769  ac6sfi  7846  iunfi  7893  indexfi  7913  dffi3  7976  nfoi  8060  ixpiunwdom  8137  cantnflem1  8225  cnfcomlem  8235  r1val1  8288  rankidb  8302  rankval4  8369  scottex  8387  scottexs  8389  scott0s  8390  cp  8393  tskwe  8415  cardmin2  8463  fseqenlem1  8486  dfac8clem  8494  cardaleph  8551  hsmexlem2  8888  axcc2  8898  ac6num  8940  ac6c4  8942  axdclem  8980  iundom2g  8996  uniimadomf  9001  cardmin  9020  pwfseqlem2  9115  pwfseqlem4a  9117  pwfseqlem4  9118  inar1  9231  lble  10591  nnwof  11259  nnwos  11260  fzrevral  11914  rabssnn0fi  12236  nfseq  12261  seqof2  12309  hashrabsn1  12591  nfwrd  12737  relexpsucnnr  13143  rlim2  13615  ello1mpt  13640  rlimcld2  13697  o1compt  13706  nfsum1  13811  nfsum  13812  sumeq2ii  13814  cbvsumv  13817  cbvsumi  13818  sumfc  13830  summolem2a  13836  zsum  13839  sumss  13845  sumss2  13847  fsumcvg2  13848  fsumzcl2  13859  fsumadd  13860  sumsn  13862  sumsns  13866  fsummsnunz  13870  fsumsplitsnun  13871  fsum2dlem  13886  fsumcom2  13890  fsumshftm  13897  fsummulc2  13900  fsum00  13913  fsumrelem  13922  fsumrlim  13926  fsumo1  13927  o1fsum  13928  fsumiun  13936  prodeq1  14018  nfcprod1  14019  nfcprod  14020  cbvprod  14024  cbvprodv  14025  cbvprodi  14026  prodmolem2a  14043  zprod  14046  fprod  14050  fprodntriv  14051  prodfc  14054  prodss  14056  fprodcllemf  14067  fprodmul  14069  fproddiv  14070  prodsn  14071  prodsnf  14073  fprodm1s  14079  fprodp1s  14080  prodsns  14081  fprodn0  14088  fprod2dlem  14089  fprodcom2  14093  fproddivf  14096  fprodsplitf  14097  fprodsplit1f  14099  fprodle  14105  fprodefsum  14204  prmind2  14690  coprmprod  14733  coprmproddvdslem  14734  pcmpt  14892  pcmptdvds  14894  prdsbas3  15434  prdsdsval2  15437  mreiincl  15557  invfuc  15934  yonedalem4b  16216  gsumconstf  17623  gsumsnd  17640  gsumsn  17642  gsumunsnd  17645  gsummpt1n0  17652  gsum2d2lem  17660  gsum2d2  17661  gsumcom2  17662  prdsgsum  17665  dprd2d2  17732  gsumdixp  17892  lss1d  18241  psrass1lem  18656  evlslem4  18786  mpfrcl  18796  coe1fzgsumdlem  18950  gsummoncoe1  18953  gsumply1eq  18954  evl1gsumdlem  18999  mdetralt2  19689  mdetunilem2  19693  madugsum  19723  gsummatr01lem4  19738  cayleyhamilton1  19971  neiptopnei  20203  fiuncmp  20474  iuncon  20498  2ndcdisj  20526  dissnlocfin  20599  elptr2  20644  ptbasfi  20651  ptunimpt  20665  ptcldmpt  20684  ptclsg  20685  ptcnplem  20691  ptcnp  20692  cnmpt11  20733  cnmpt1t  20735  cnmpt21  20741  cnmpt2t  20743  cnmptcom  20748  cnmptk2  20756  cnmpt2k  20758  imasnopn  20760  imasncld  20761  imasncls  20762  xkocnv  20884  elmptrab  20897  flfcnp2  21077  ptcmpg  21127  fmucnd  21362  prdsdsf  21437  prdsxmet  21439  cfilucfil  21629  blval2  21632  restmetu  21640  fsumcn  21957  fsum2cn  21958  ovolfiniun  22509  ovoliunlem3  22512  ovoliun  22513  ovoliun2  22514  ovoliunnul  22515  finiunmbl  22553  volfiniun  22556  iundisj  22557  iundisj2  22558  iunmbl  22562  voliun  22563  iunmbl2  22566  mbfpos  22663  mbfposr  22664  mbfposb  22665  mbfsup  22676  mbfinf  22677  mbfinfOLD  22678  mbflim  22682  i1fposd  22721  itg1climres  22728  itg2splitlem  22762  itg2split  22763  itg2cnlem1  22775  isibl2  22780  itgeq1  22786  nfitg1  22787  nfitg  22788  cbvitg  22789  cbvitgv  22790  itgmpt  22796  itgss3  22828  itgfsum  22840  itgabs  22848  itggt0  22855  itgcn  22856  cbvditgv  22866  limcmpt  22894  limciun  22905  dvmptfsum  22983  dvlipcn  23002  lhop2  23023  dvfsumle  23029  dvfsumabs  23031  dvfsumlem1  23034  dvfsumlem2  23035  dvfsumlem4  23037  dvfsumrlim  23039  dvfsum2  23042  itgparts  23055  itgsubstlem  23056  itgsubst  23057  elplyd  23212  coeeq2  23252  dgrle  23253  ulmss  23408  itgulm2  23420  leibpi  23924  rlimcnp  23947  rlimcnp2  23948  o1cxp  23956  lgamgulmlem2  24011  lgamgulmlem6  24015  lgamgulm2  24017  fsumdvdscom  24170  fsumdvdsmul  24180  fsumvma  24197  lgseisenlem2  24334  dchrisumlema  24382  dchrisumlem2  24384  dchrisumlem3  24385  nbgraopALT  25208  cnlnadjlem5  27780  chirred  28104  vtocl2d  28165  ralcom4f  28166  rexcom4f  28167  rmo4fOLD  28188  rabtru  28191  iunin1f  28226  iunxsngf  28227  disji2f  28241  disjorsf  28244  disjif2  28245  disjabrex  28246  disjabrexf  28247  iundisjf  28253  iundisj2f  28254  disjunsn  28258  ac6sf2  28279  dfimafnf  28286  suppss2fOLD  28290  suppss2f  28291  fimarab  28297  fmptdF  28308  resmptf  28310  fmptcof2  28311  fcomptf  28312  acunirnmpt2  28314  acunirnmpt2f  28315  aciunf1lem  28316  aciunf1  28317  ofpreima  28320  funcnvmptOLD  28322  funcnvmpt  28323  funcnv5mpt  28324  funcnv4mpt  28325  f1od2  28361  fpwrelmap  28370  fpwrelmapffs  28371  xrofsup  28405  iundisjfi  28424  iundisj2fi  28425  iundisjcnt  28426  iundisj2cnt  28427  nnindf  28434  gsummpt2co  28594  gsumvsca1  28596  gsumvsca2  28597  mdetpmtr1  28700  ordtconlem1  28781  qqhval2  28837  esumcl  28902  nfesum1  28912  nfesum2  28913  cbvesumv  28915  esumid  28916  esumgsum  28917  esumval  28918  esumel  28919  esumnul  28920  esumc  28923  esumrnmpt  28924  esumsplit  28925  esummono  28926  esumpad  28927  esumpad2  28928  esumadd  28929  esumle  28930  gsumesum  28931  esumlub  28932  esumaddf  28933  esumsnf  28936  esumsn  28937  esumpr  28938  esumrnmpt2  28940  esumfzf  28941  esumfsup  28942  esumss  28944  esumpinfval  28945  esumpfinvalf  28948  esumpinfsum  28949  esumpcvgval  28950  esumpmono  28951  esumcocn  28952  esummulc1  28953  esummulc2  28954  esumdivc  28955  esumcvg  28958  esumsup  28961  esumgect  28962  esum2dlem  28964  esum2d  28965  esumiun  28966  sigaclcu2  28993  ldsysgenld  29033  sigapildsys  29035  ldgenpisyslem1  29036  fiunelros  29047  measvunilem  29085  measvunilem0  29086  measvuni  29087  measiuns  29090  measiun  29091  meascnbl  29092  voliune  29102  volfiniune  29103  volmeas  29104  ddemeas  29109  imambfm  29134  omscl  29169  omsclOLD  29173  oms0  29175  omsmon  29176  omssubadd  29178  oms0OLD  29179  omsmonOLD  29180  omssubaddOLD  29182  carsgclctunlem1  29199  carsggect  29200  carsgclctunlem2  29201  omsmeas  29205  omsmeasOLD  29206  sibfof  29223  eulerpartlemn  29264  bnj23  29574  bnj1366  29691  bnj1400  29697  bnj1534  29714  bnj1542  29718  bnj607  29777  bnj873  29785  bnj958  29801  bnj1000  29802  bnj981  29811  bnj1014  29821  bnj1123  29845  bnj1204  29871  bnj1388  29892  bnj1398  29893  bnj1408  29895  bnj1445  29903  bnj1446  29904  bnj1447  29905  bnj1448  29906  bnj1449  29907  bnj1466  29912  bnj1467  29913  bnj1463  29914  bnj1312  29917  bnj1498  29920  bnj1519  29924  bnj1520  29925  bnj1525  29928  bnj1529  29929  cvmcov  30036  setinds  30474  dfon2lem3  30481  tfisg  30507  trpredlem1  30518  trpredtr  30521  trpredmintr  30522  trpred0  30527  trpredrec  30529  frinsg  30533  nfwlim  30555  sltval2  30593  nobndlem5  30635  finminlem  31024  bj-rabtrALT  31580  topdifinfindis  31795  topdifinffinlem  31796  isbasisrelowllem1  31804  isbasisrelowllem2  31805  iooelexlt  31811  relowlssretop  31812  finxpreclem2  31828  finxpreclem6  31834  phpreu  31975  finixpnum  31976  ptrest  31985  poimirlem16  32002  poimirlem19  32005  poimirlem23  32009  poimirlem24  32010  poimirlem25  32011  poimirlem26  32012  poimirlem27  32013  poimirlem28  32014  mbfposadd  32034  dvtanlemOLD  32037  itgabsnc  32057  itggt0cn  32060  ftc1cnnclem  32061  ftc1anclem5  32067  ftc2nc  32072  indexa  32106  indexdom  32107  filbcmb  32113  sdclem2  32117  sdclem1  32118  fdc1  32121  totbndbnd  32167  heibor1  32188  scottexf  32457  scott0f  32458  ac6s6f  32462  fsumshftd  32569  fsumshftdOLD  32570  riotasvd  32574  riotasv2d  32575  riotasv2s  32576  riotaocN  32821  cdleme26ee  33973  cdleme31sn1  33994  cdleme31se2  33996  cdlemefrs29bpre0  34009  cdlemefs32sn1aw  34027  cdleme43fsv1snlem  34033  cdleme41sn3a  34046  cdleme32d  34057  cdleme32f  34059  cdleme40m  34080  cdleme40n  34081  cdleme42b  34091  ltrniotaval  34194  cdlemksv2  34460  cdlemkuv2  34480  cdlemk36  34526  cdlemk38  34528  cdlemkid  34549  cdlemk19x  34556  cdlemk11t  34559  dihglblem5  34912  hlhilset  35551  elrfirn2  35584  mzpsubst  35636  eq0rabdioph  35665  sbcrexgOLD  35674  sbccomieg  35682  rexrabdioph  35683  rexfrabdioph  35684  rabdiophlem2  35691  elnn0rabdioph  35692  dvdsrabdioph  35699  rabrenfdioph  35703  monotoddzz  35837  oddcomabszz  35838  setindtrs  35926  wdom2d2  35936  aomclem6  35963  aomclem8  35965  areaquad  36147  ss2iundv  36298  cbviuneq12dv  36300  binomcxplemdvbinom  36747  binomcxplemdvsum  36749  binomcxplemnotnn0  36750  compab  36839  iunconlem2  37373  evth2f  37377  elunif  37378  fvelrnbf  37380  rfcnpre1  37381  fsumcnf  37383  sumsnd  37388  evthf  37389  refsumcn  37392  rfcnpre2  37393  rfcnpre3  37395  rfcnpre4  37396  rfcnnnub  37398  refsum2cnlem1  37399  refsum2cn  37400  uzwo4  37431  iunxsngf2  37441  fiiuncl  37445  inn0  37458  dfcleqf  37471  iunssf  37481  suprnmpt  37493  dffo3f  37504  elrnmptf  37508  disjf1  37511  wessf1ornlem  37513  disjrnmpt2  37517  disjf1o  37520  fompt  37521  disjinfi  37522  choicefi  37535  iunmapss  37553  ssmapsn  37554  iunmapsn  37555  ssfiunibd  37602  supxrgere  37631  iuneqfzuzlem  37632  supxrgelem  37635  supxrge  37636  infxrunb2  37667  fsumclf  37730  fsumsplitf  37731  fsummulc1f  37732  sumsnf  37733  fsumsplit1  37736  fsumf1of  37738  fsumiunss  37739  fsumreclf  37740  fsumlessf  37741  fsumsermpt  37743  fmul01  37744  fmuldfeqlem1  37746  fmuldfeq  37747  fmul01lt1lem1  37748  fmul01lt1lem2  37749  fmul01lt1  37750  cncfmptss  37751  mulc1cncfg  37753  infrglbOLD  37755  expcnfg  37757  fprodexp  37760  fprodabs2  37761  mccllem  37763  mccl  37764  climmulf  37768  climexp  37769  climsuse  37773  climrecf  37774  climinff  37776  climinffOLD  37777  climaddf  37781  mullimc  37782  constlimc  37790  idlimc  37792  limcperiod  37794  sumnnodd  37796  neglimc  37814  addlimc  37815  0ellimcdiv  37816  cncfshift  37837  icccncfext  37851  cncficcgt0  37852  cncfiooicclem1  37857  fprodcncf  37865  dvcosre  37867  dvmptmulf  37898  dvnmptdivc  37899  dvnmul  37904  dvmptfprodlem  37905  dvmptfprod  37906  dvnprodlem1  37907  dvnprodlem2  37908  itgsin0pilem1  37912  ibliccsinexp  37913  itgsinexplem1  37916  itgsinexp  37917  iblsplitf  37933  itgsubsticclem  37938  volioofmpt  37958  volicofmpt  37961  stoweidlem3  37964  stoweidlem14  37975  stoweidlem16  37977  stoweidlem18  37979  stoweidlem21  37982  stoweidlem23  37984  stoweidlem26  37987  stoweidlem27  37988  stoweidlem28  37989  stoweidlem29  37990  stoweidlem29OLD  37991  stoweidlem31  37993  stoweidlem34  37996  stoweidlem35  37997  stoweidlem36  37998  stoweidlem41  38003  stoweidlem42  38004  stoweidlem43  38005  stoweidlem46  38008  stoweidlem47  38009  stoweidlem48  38010  stoweidlem51  38013  stoweidlem52  38014  stoweidlem53  38015  stoweidlem54  38016  stoweidlem55  38017  stoweidlem56  38018  stoweidlem57  38019  stoweidlem58  38020  stoweidlem59  38021  stoweidlem60  38022  stoweidlem62  38024  stoweidlem62OLD  38025  stowei  38027  wallispilem5  38032  stirlinglem4  38040  stirlinglem5  38041  stirlinglem11  38047  stirlinglem12  38048  stirlinglem13  38049  stirlinglem14  38050  stirlinglem15  38051  stirling  38052  fourierdlem20  38090  fourierdlem31  38101  fourierdlem31OLD  38102  fourierdlem48  38119  fourierdlem51  38122  fourierdlem68  38139  fourierdlem73  38144  fourierdlem79  38150  fourierdlem80  38151  fourierdlem86  38157  fourierdlem89  38160  fourierdlem91  38162  fourierdlem103  38174  fourierdlem104  38175  fourierdlem112  38183  fourierdlem115  38186  fourierd  38187  fourierclimd  38188  etransclem2  38202  etransclem24  38224  etransclem25  38225  etransclem26  38226  etransclem28  38228  etransclem32  38232  etransclem35  38235  etransclem37  38237  etransclem44  38244  etransclem46  38246  etransclem48OLD  38248  etransclem48  38249  sge00  38321  sge0revalmpt  38323  sge0f1o  38327  sge0fsummpt  38335  sge0pnffigt  38341  sge0lefi  38343  sge0ltfirp  38345  sge0resplit  38351  sge0lempt  38355  sge0iunmptlemfi  38358  sge0iunmptlemre  38360  sge0fodjrnlem  38361  sge0iunmpt  38363  sge0ltfirpmpt2  38371  sge0isummpt2  38377  sge0xaddlem2  38379  sge0xadd  38380  sge0fsummptf  38381  sge0gtfsumgt  38388  iundjiun  38403  meadjiun  38409  voliunsge0lem  38415  omeiunle  38446  omeiunltfirp  38448  carageniuncllem1  38450  caratheodorylem1  38455  caratheodorylem2  38456  hoicvrrex  38485  ovnlerp  38491  ovncvrrp  38493  ovn0lem  38494  hoidmvval0  38516  hoidmvlelem1  38524  hoidmvlelem3  38526  ovnhoilem1  38530  ovnlecvr2  38539  hspdifhsp  38545  hoiqssbllem2  38552  hspmbllem1  38555  hspmbllem2  38556  opnvonmbllem1  38561  opnvonmbllem2  38562  ovnsubadd2lem  38574  ovolval5lem2  38582  ovnovollem1  38585  ovnovollem2  38586  vonvolmbllem  38589  cbvral2  38728  cbvrex2  38729  raaan2  38731  2reurex  38737  2reu3  38744  2reu7  38747  2reu8  38748  eu2ndop1stv  38758  nfafv  38773  iunopeqop  39141  fsummsndifre  39233  fsumsplitsndif  39234  fsummmodsndifre  39235  fsummmodsnunz  39236  gropd  39275  grstructd  39276  opeliun2xp  40483  dmmpt2ssx2  40487  ovmpt2rdxf  40489  ovmpt2rdx  40490  aacllem  40909
  Copyright terms: Public domain W3C validator