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

Theorem eleqtrrd 2888
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eleqtrrd.1 (𝜑𝐴𝐵)
eleqtrrd.2 (𝜑𝐶 = 𝐵)
Assertion
Ref Expression
eleqtrrd (𝜑𝐴𝐶)

Proof of Theorem eleqtrrd
StepHypRef Expression
1 eleqtrrd.1 . 2 (𝜑𝐴𝐵)
2 eleqtrrd.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2812 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrd 2887 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799  df-clel 2802
This theorem is referenced by:  3eltr4d  2900  disjxiun  4841  eldmressnsn  5644  elimdelov  6966  elovmpt3rab1  7123  fnwelem  7526  tfrlem13  7722  tz7.44-2  7739  omordi  7883  oneo  7898  omeulem2  7900  oeordi  7904  oeeui  7919  nnneo  7968  erref  7999  en1uniel  8264  omxpenlem  8300  unblem3  8453  dffi3  8576  ordtypelem10  8671  oismo  8684  cantnff  8818  cantnfp1lem3  8824  cantnflem1  8833  cnfcom  8844  r1ordg  8888  r1pwss  8894  rankwflemb  8903  r1elwf  8906  rankidb  8910  rankonidlem  8938  fseqenlem2  9131  dfac12lem1  9250  dfac12lem2  9251  pwsdompw  9311  ackbij2lem3  9348  ackbij2  9350  cfsmolem  9377  isfin4-3  9422  hsmexlem4  9536  ttukeylem3  9618  ttukeylem7  9622  iundom2g  9647  fpwwe2lem9  9745  canthwelem  9757  pwfseqlem4  9769  winalim2  9803  r1wunlim  9844  tskmid  9947  fzopth  12601  predfz  12688  fzoss2  12720  fz1fzo0m1  12740  fzo0addel  12746  fzo0addelr  12747  fzosubel3  12753  elfzomin  12764  elfzonlteqm1  12768  fzoend  12783  fzofzp1  12789  fzofzp1b  12790  peano2fzor  12799  zmodfzo  12917  seqf1olem2  13064  bcn2  13326  swrdccat2  13682  swrdswrd  13684  swrdccatin12  13715  splfv1  13730  revcl  13734  revlen  13735  revccat  13739  revrev  13740  cshwidxmod  13773  revco  13804  limsupgre  14435  summolem2a  14669  fsumm1  14703  fsumcom2  14728  prodmolem2a  14885  fprodm1  14918  fprodcom2  14935  prmreclem4  15840  prmreclem5  15841  vdwapid1  15896  vdwlem5  15906  vdwlem8  15909  vdwnnlem2  15917  ramub1lem1  15947  ramub1lem2  15948  mrieqvlemd  16494  mreexd  16507  mreexexlemd  16509  catcocl  16550  catass  16551  moni  16600  epii  16607  inviso1  16630  episect  16649  invisoinvl  16654  catsubcat  16703  subccocl  16709  fullsubc  16714  funcco  16735  resf2nd  16759  funcres  16760  fthepi  16792  nati  16819  arwhoma  16899  catccatid  16956  resscatc  16959  catcisolem  16960  catcoppccl  16962  catcfuccl  16963  estrreslem2  16982  funcestrcsetclem3  16987  funcestrcsetclem8  16992  equivestrcsetc  16997  funcsetcestrclem3  17001  funcsetcestrclem8  17007  xpcco  17028  xpcco2  17032  xpccatid  17033  prfcl  17048  catcxpccl  17052  curf12  17072  curf1cl  17073  curf2  17074  curf2cl  17076  curfcl  17077  uncf2  17082  uncfcurf  17084  diag12  17089  diag2  17090  curf2ndf  17092  hofcl  17104  oppchofcl  17105  oyoncl  17115  yonedalem3a  17119  yonedalem4b  17121  yonedalem22  17123  yonedalem3b  17124  yonedalem3  17125  yonedainv  17126  yonffthlem  17127  latcl2  17253  latlem  17254  latjcom  17264  latmcom  17280  clatlem  17316  clatlubcl2  17318  clatglbcl2  17320  acsfiindd  17382  gsumpropd2lem  17478  mndpropd  17521  imasmnd  17533  frmdmnd  17601  frmdgsum  17604  grpsubpropd2  17726  imasgrp  17736  subg0  17802  0ghm  17876  resghm2  17879  ghmco  17882  pwsdiagghm  17890  psgnunilem1  18114  psgnunilem5  18115  psgnunilem2  18116  psgnunilem3  18117  sylow1lem4  18217  sylow1lem5  18218  efglem  18330  efgtf  18336  efginvrel2  18341  efginvrel1  18342  efgsdmi  18346  efgs1b  18350  efgsres  18352  efgsfo  18353  efgredleme  18357  efgredlemc  18359  efgredlem  18361  efgcpbllemb  18369  frgp0  18374  frgpadd  18377  frgpinv  18378  vrgpf  18382  vrgpinv  18383  frgpuplem  18386  frgpup1  18389  frgpup2  18390  frgpup3lem  18391  frgpnabllem1  18477  frgpnabllem2  18478  gsumval3  18509  dprdfid  18618  dprdsn  18637  dprd2da  18643  dpjidcl  18659  pgpfac1lem2  18676  pgpfaclem3  18684  ringpropd  18784  imasring  18821  qusring2  18822  pwsco1rhm  18942  pwsco2rhm  18943  subrgunit  19002  pwsdiagrhm  19017  isabvd  19024  lmodprop2d  19129  islssd  19140  prdsvscacl  19175  prdslmodd  19176  islmhm2  19245  lmhmco  19250  lmhmplusg  19251  lmhmvsca  19252  lmhmpropd  19280  lsppreli  19297  lspsnel4  19331  lssacsex  19352  lspsnat  19353  qus1  19444  qusrhm  19446  assapropd  19536  psr0cl  19603  psrnegcl  19605  psr1cl  19611  resspsrmul  19626  subrgpsr  19628  mvrf  19633  mplmon  19672  mplcoe1  19674  subrgasclcl  19707  mplind  19710  evlslem1  19723  subrgply1  19811  psrplusgpropd  19814  ply1coe  19874  cply1coe0bi  19878  lply1binomsc  19885  evls1val  19893  evls1rhm  19895  evl1val  19901  evl1rhm  19904  pf1ind  19927  evl1scvarpw  19935  znf1o  20107  cssmre  20247  dsmmlss  20298  frlmsplit2  20322  frlmbas3  20325  frlmup1  20347  matbas2i  20438  matplusg2  20443  matvsca2  20444  matsubgcell  20450  matvscacell  20452  mpt2matmul  20463  mavmulval  20562  mavmulcl  20564  mavmulass  20566  mavmul0  20569  mavmumamul1  20572  m1detdiag  20614  cramerimplem2  20703  mat2pmatmul  20749  mat2pmatlin  20753  monmatcollpw  20797  pmatcollpwfi  20800  mply1topmatcl  20823  pm2mpghm  20834  pm2mpmhmlem2  20837  pm2mp  20843  chpmat1dlem  20853  chpmat1d  20854  chpdmatlem0  20855  chpscmat  20860  chpscmatgsumbin  20862  chpscmatgsummon  20863  chfacfscmulcl  20875  cpmadugsumlemB  20892  cpmadugsumlemC  20893  chcoeffeqlem  20903  cldmreon  21112  neiptopreu  21151  maxlp  21165  ordttopon  21211  ordtrest2lem  21221  cnprcl2  21269  lmcnp  21322  resthauslem  21381  hauscmplem  21423  1stcfb  21462  2ndcctbss  21472  2ndcomap  21475  dis2ndc  21477  loclly  21504  hausllycmp  21511  locfincmp  21543  dissnref  21545  kgeni  21554  kgenidm  21564  ptpjpre2  21597  xkoopn  21606  txopn  21619  ptpjopn  21629  ptcldmpt  21631  ptcls  21633  pthaus  21655  txkgen  21669  xkohaus  21670  xkopt  21672  txconn  21706  imastps  21738  kqid  21745  kqopn  21751  kqcld  21752  isr0  21754  indishmph  21815  pt1hmeo  21823  ptuncnv  21824  ptunhmeo  21825  t0kq  21835  filconn  21900  uzrest  21914  uffixsn  21942  fmfnfmlem2  21972  flimss2  21989  flimss1  21990  flimclslem  22001  flfcnp  22021  fclsfnflim  22044  uffclsflim  22048  fcfelbas  22053  alexsublem  22061  alexsub  22062  cnextcn  22084  cnextfres1  22085  tmdgsum  22112  distgp  22116  indistgp  22117  symgtgp  22118  ghmcnp  22131  qustgpopn  22136  qustgplem  22137  qustgphaus  22139  prdstmdd  22140  prdstgpd  22141  tsmsid  22156  tsmssubm  22159  tsmsmhm  22162  tsmsadd  22163  tsmssplit  22168  utop2nei  22267  utop3cls  22268  neipcfilu  22313  cnextucn  22320  ucnextcn  22321  blpnfctr  22454  lpbl  22521  met2ndci  22540  tmsxps  22554  metcnpi  22562  metcnpi2  22563  metcnpi3  22564  metustid  22572  metustsym  22573  metustexhalf  22574  subgngp  22652  ngptgp  22653  sranlm  22701  nlmvscn  22704  nrginvrcn  22709  lssnlm  22718  nghmcn  22762  iccntr  22837  icccmplem2  22839  msdcn  22857  cncfmptc  22927  cncfmptid  22928  cncfmpt2f  22930  icoopnst  22951  iocopnst  22952  nmoleub2lem3  23127  nmoleub3  23131  nmhmcn  23132  ipcn  23257  cfilfcls  23284  caucfil  23293  equivcau  23310  caubl  23318  flimcfil  23324  rrxdstprj1  23404  minveclem3b  23411  minveclem4  23415  ovolicc2lem3  23500  ovolicc2lem4  23501  opnmbllem  23582  vitalilem2  23590  mbfsup  23645  mbfinf  23646  mbfi1fseqlem4  23699  limccnp  23869  limccnp2  23870  dvreslem  23887  dvres2lem  23888  dvidlem  23893  dvcnp2  23897  dvcn  23898  dvaddbr  23915  dvmulbr  23916  dvcmul  23921  dvcof  23925  dvcnvlem  23953  dvef  23957  rollelem  23966  dvlip2  23972  dvivthlem1  23985  dvivth  23987  lhop2  23992  lhop  23993  dvcnvrelem1  23994  dvcnvrelem2  23995  dvcnvre  23996  ply1rem  24137  fta1blem  24142  plycpn  24258  plyrem  24274  tayl0  24330  dvtaylp  24338  dvntaylp  24339  dvntaylp0  24340  taylthlem1  24341  taylthlem2  24342  ulmdvlem3  24370  psercn  24394  pserdv  24397  abelth  24409  efabl  24511  efopnlem1  24616  loglesqrt  24713  relogbf  24743  efrlim  24910  dchrghm  25195  dchrptlem3  25205  tgbtwntriv2  25596  tgbtwnne  25599  ercgrg  25626  tgidinside  25680  tgbtwnconn1  25684  tglnne  25737  tglnne0  25749  tglnpt2  25750  tglineneq  25753  ncolncol  25755  coltr3  25757  mirln  25785  mirln2  25786  mirconn  25787  krippenlem  25799  footex  25827  colperpexlem3  25838  mideulem2  25840  opphllem  25841  oppne3  25849  opphllem1  25853  opphllem2  25854  opphllem4  25856  oppperpex  25859  opphl  25860  hlpasch  25862  hpgerlem  25871  colhp  25876  midbtwn  25885  lmieu  25890  lmiisolem  25902  sacgr  25936  f1otrg  25965  f1otrge  25966  ebtwntg  26076  ecgrtg  26077  eengtrkg  26079  eengtrkge  26080  upgr1eop  26224  usgredg3  26323  uspgr1eop  26355  usgr1eop  26358  vtxdun  26605  vtxdfiun  26606  1loopgruspgr  26624  1loopgrvd2  26627  1hevtxdg1  26630  1egrvtxdg1  26633  1egrvtxdg0  26635  umgr2v2e  26649  wlkres  26795  wlkp1lem4  26801  wlkp1  26806  wwlksm1edg  27008  wwlksnext  27030  wwlksnextproplem3  27049  clwwlkccatlem  27132  clwwlkel  27195  1wlkdlem2  27311  trlsegvdeg  27400  eupth2lem3lem1  27401  eupth2lem3lem2  27402  rspc2vd  27440  extwwlkfab  27531  numclwlk2lem2f  27557  numclwlk2lem2fOLD  27564  spansnid  28750  elspansn4  28760  submarchi  30065  psgnfzto1stlem  30175  1smat1  30195  submat1n  30196  lmatfval  30205  lmatcl  30207  mdetpmtr1  30214  madjusmdetlem4  30221  qtopt1  30227  qtophaus  30228  locfinref  30233  ordtrest2NEWlem  30293  elzrhunit  30348  qqhcn  30360  qqhucn  30361  esumel  30434  esumsplit  30440  sigagenss2  30538  elsx  30582  sxbrsigalem0  30658  dya2icoseg  30664  eulerpartlemb  30755  eulerpartlemgvv  30763  iwrdsplit  30774  sseqfv2  30781  probfinmeasb  30816  dstrvprob  30858  dstfrvel  30860  ballotlemrv  30906  signstfvn  30971  signstfvp  30973  signstfveq0  30979  signsvtp  30985  signsvtn  30986  reprsuc  31018  reprpmtf1o  31029  bnj1006  31352  bnj1018  31355  bnj1121  31376  bnj1398  31425  bnj1450  31441  bnj1501  31458  subfacp1lem5  31489  ptpconn  31538  indispconn  31539  cvxsconn  31548  cvmseu  31581  cvmliftmolem2  31587  cvmliftlem7  31596  cvmliftlem10  31599  cvmliftlem13  31601  cvmlift2lem12  31619  mrsubcv  31730  mrsubff  31732  mrsubrn  31733  mrsubccat  31738  elmrsubrn  31740  mrsubco  31741  mrsubvrs  31742  mvhf  31778  msubvrs  31780  mclsax  31789  frrlem11  32113  nodenselem5  32159  nosupres  32174  linerflx1  32577  linerflx2  32579  fwddifnval  32591  elhf2  32603  neibastop2lem  32676  icoreunrn  33523  relowlssretop  33527  sucneqond  33529  matunitlindflem2  33719  poimirlem4  33726  poimirlem20  33742  poimirlem30  33752  broucube  33756  opnmbllem0  33758  areacirclem2  33813  areacirclem4  33815  blssp  33863  sstotbnd2  33884  totbndbnd  33899  prdstotbnd  33904  cnpwstotbnd  33907  heiborlem9  33929  exidcl  33986  exidresid  33989  grpokerinj  34003  iscringd  34108  prter3  34661  toycom  34753  islfld  34842  lshpsmreu  34889  ldualelvbase  34907  ldualssvscl  34938  lkreqN  34950  lkrlspeqN  34951  erng1lem  36768  erngdvlem4  36772  erng0g  36775  erng1r  36776  erngdvlem4-rN  36780  dva0g  36808  dia1dim2  36843  dia1dimid  36844  dia2dimlem5  36849  dvhelvbasei  36869  dvhvaddass  36878  tendoinvcl  36885  tendolinv  36886  tendorinv  36887  dvhgrp  36888  dvhlveclem  36889  cdlemn4  36979  lcfrlem12N  37335  lcfrlem15  37338  lcdvscl  37386  lcdlssvscl  37387  lcdvsass  37388  lcdvs0N  37397  mapdincl  37442  mapdin  37443  mapdlsmcl  37444  mapdcnvatN  37447  mapdpglem2  37454  mapdpglem12  37464  mapdpglem18  37470  mapdpglem21  37473  mapdpglem22  37474  mapdpglem28  37482  mapdpglem30  37483  hdmaprnlem3N  37631  hdmaprnlem3uN  37632  hdmaprnlem7N  37636  hdmaprnlem8N  37637  hdmaprnlem9N  37638  hdmaprnlem3eN  37639  hdmaprnlem16N  37643  hgmapdcl  37671  hgmapval1  37674  hgmaprnlem4N  37680  hdmapinvlem1  37699  wepwsolem  38113  kercvrlsm  38154  dfacbasgrp  38179  cntzsdrg  38273  imo72b2lem0  38965  dvconstbi  39033  cncmpmax  39685  iooabslt  40205  fmul01lt1lem2  40297  limciccioolb  40333  limcicciooub  40349  limsuppnfdlem  40413  climrescn  40460  climxrrelem  40461  climxrre  40462  xlimmnfvlem2  40539  xlimpnfvlem2  40543  fsumcncf  40571  ioccncflimc  40578  icocncflimc  40582  cncfiooicclem1  40586  dvbdfbdioolem2  40624  dvnmul  40638  stoweidlem26  40722  stoweidlem34  40730  stoweidlem48  40744  stoweidlem59  40755  dirkercncflem3  40801  fourierdlem32  40835  fourierdlem41  40844  fourierdlem51  40853  fourierdlem63  40865  fourierdlem82  40884  fourierdlem85  40887  fourierdlem93  40895  fourierdlem111  40913  fourierdlem114  40916  etransclem35  40965  hspdifhsp  41312  opnvonmbllem1  41328  ovnovollem1  41352  mbfresmf  41430  smfaddlem1  41453  smfsuplem1  41499  smflimsuplem5  41512  fzoopth  41912  setsidel  41921  setsnidel  41922  pfxccat1  41985  pfxccatin12  42000  repswpfx  42011  prelspr  42304  rnghmsubcsetclem1  42543  rngccatidALTV  42557  zrinitorngc  42568  zrtermorngc  42569  zrzeroorngc  42570  rhmsubcsetclem1  42589  rhmsubcrngclem1  42595  funcringcsetcALTV2lem3  42606  funcringcsetcALTV2lem8  42611  ringccatidALTV  42620  funcringcsetclem3ALTV  42629  funcringcsetclem8ALTV  42634  irinitoringc  42637  zrtermoringc  42638  zrninitoringc  42639  nzerooringczr  42640  srhmsubclem2  42642  srhmsubc  42644  srhmsubcALTVlem1  42660  srhmsubcALTV  42662  rhmsubcALTVlem3  42674  lcosslsp  42795  nnolog2flm1  42952
  Copyright terms: Public domain W3C validator