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

Theorem eleqtrrd 2733
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 2657 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrd 2732 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  3eltr4d  2745  disjxiun  4681  disjxiunOLD  4682  eldmressnsn  5474  elimdelov  6778  elovmpt3rab1  6935  fnwelem  7337  tfrlem13  7531  tz7.44-2  7548  omordi  7691  oneo  7706  omeulem2  7708  oeordi  7712  oeeui  7727  nnneo  7776  erref  7807  en1uniel  8069  omxpenlem  8102  unblem3  8255  dffi3  8378  ordtypelem10  8473  oismo  8486  cantnff  8609  cantnfp1lem3  8615  cantnflem1  8624  cnfcom  8635  r1ordg  8679  r1pwss  8685  rankwflemb  8694  r1elwf  8697  rankidb  8701  rankonidlem  8729  fseqenlem2  8886  dfac12lem1  9003  dfac12lem2  9004  pwsdompw  9064  ackbij2lem3  9101  ackbij2  9103  cfsmolem  9130  isfin4-3  9175  hsmexlem4  9289  ttukeylem3  9371  ttukeylem7  9375  iundom2g  9400  fpwwe2lem9  9498  canthwelem  9510  pwfseqlem4  9522  winalim2  9556  r1wunlim  9597  tskmid  9700  fzopth  12416  predfz  12503  fzoss2  12535  fz1fzo0m1  12555  fzo0addel  12561  fzo0addelr  12562  fzosubel3  12568  elfzomin  12579  elfzonlteqm1  12583  fzoend  12599  fzofzp1  12605  fzofzp1b  12606  peano2fzor  12615  zmodfzo  12733  seqf1olem2  12881  bcn2  13146  swrdccat2  13504  swrdswrd  13506  swrdccatin12  13537  splfv1  13552  revcl  13556  revlen  13557  revccat  13561  revrev  13562  cshwidxmod  13595  revco  13626  limsupgre  14256  summolem2a  14490  fsumm1  14524  fsumcom2  14549  fsumcom2OLD  14550  prodmolem2a  14708  fprodm1  14741  fprodcom2  14758  fprodcom2OLD  14759  prmreclem4  15670  prmreclem5  15671  vdwapid1  15726  vdwlem5  15736  vdwlem8  15739  vdwnnlem2  15747  ramub1lem1  15777  ramub1lem2  15778  mrieqvlemd  16336  mreexd  16349  mreexexlemd  16351  catcocl  16393  catass  16394  moni  16443  epii  16450  inviso1  16473  episect  16492  invisoinvl  16497  catsubcat  16546  subccocl  16552  fullsubc  16557  funcco  16578  resf2nd  16602  funcres  16603  fthepi  16635  nati  16662  arwhoma  16742  catccatid  16799  resscatc  16802  catcisolem  16803  catcoppccl  16805  catcfuccl  16806  estrreslem2  16825  funcestrcsetclem3  16829  funcestrcsetclem8  16834  equivestrcsetc  16839  funcsetcestrclem3  16843  funcsetcestrclem8  16849  xpcco  16870  xpcco2  16874  xpccatid  16875  prfcl  16890  catcxpccl  16894  curf12  16914  curf1cl  16915  curf2  16916  curf2cl  16918  curfcl  16919  uncf2  16924  uncfcurf  16926  diag12  16931  diag2  16932  curf2ndf  16934  hofcl  16946  oppchofcl  16947  oyoncl  16957  yonedalem3a  16961  yonedalem4b  16963  yonedalem22  16965  yonedalem3b  16966  yonedalem3  16967  yonedainv  16968  yonffthlem  16969  latcl2  17095  latlem  17096  latjcom  17106  latmcom  17122  clatlem  17158  clatlubcl2  17160  clatglbcl2  17162  acsfiindd  17224  gsumpropd2lem  17320  mndpropd  17363  imasmnd  17375  frmdmnd  17443  frmdgsum  17446  grpsubpropd2  17568  imasgrp  17578  subg0  17647  0ghm  17721  resghm2  17724  ghmco  17727  pwsdiagghm  17735  psgnunilem1  17959  psgnunilem5  17960  psgnunilem2  17961  psgnunilem3  17962  sylow1lem4  18062  sylow1lem5  18063  efglem  18175  efgtf  18181  efginvrel2  18186  efginvrel1  18187  efgsdmi  18191  efgs1b  18195  efgsres  18197  efgsfo  18198  efgredleme  18202  efgredlemc  18204  efgredlem  18206  efgcpbllemb  18214  frgp0  18219  frgpadd  18222  frgpinv  18223  vrgpf  18227  vrgpinv  18228  frgpuplem  18231  frgpup1  18234  frgpup2  18235  frgpup3lem  18236  frgpnabllem1  18322  frgpnabllem2  18323  gsumval3  18354  dprdfid  18462  dprdsn  18481  dprd2da  18487  dpjidcl  18503  pgpfac1lem2  18520  pgpfaclem3  18528  ringpropd  18628  imasring  18665  qusring2  18666  pwsco1rhm  18786  pwsco2rhm  18787  subrgunit  18846  pwsdiagrhm  18861  isabvd  18868  lmodprop2d  18973  islssd  18984  prdsvscacl  19016  prdslmodd  19017  islmhm2  19086  lmhmco  19091  lmhmplusg  19092  lmhmvsca  19093  lmhmpropd  19121  lsppreli  19138  lspsnel4  19172  lssacsex  19192  lspsnat  19193  qus1  19283  qusrhm  19285  assapropd  19375  psr0cl  19442  psrnegcl  19444  psr1cl  19450  resspsrmul  19465  subrgpsr  19467  mvrf  19472  mplmon  19511  mplcoe1  19513  subrgasclcl  19547  mplind  19550  evlslem1  19563  subrgply1  19651  psrplusgpropd  19654  ply1coe  19714  cply1coe0bi  19718  lply1binomsc  19725  evls1val  19733  evls1rhm  19735  evl1val  19741  evl1rhm  19744  pf1ind  19767  evl1scvarpw  19775  znf1o  19948  cssmre  20085  dsmmlss  20136  frlmsplit2  20160  frlmbas3  20163  frlmup1  20185  matbas2i  20276  matplusg2  20281  matvsca2  20282  matsubgcell  20288  matvscacell  20290  mpt2matmul  20300  mavmulval  20399  mavmulcl  20401  mavmulass  20403  mavmul0  20406  mavmumamul1  20409  m1detdiag  20451  cramerimplem2  20538  mat2pmatmul  20584  mat2pmatlin  20588  monmatcollpw  20632  pmatcollpwfi  20635  mply1topmatcl  20658  pm2mpghm  20669  pm2mpmhmlem2  20672  pm2mp  20678  chpmat1dlem  20688  chpmat1d  20689  chpdmatlem0  20690  chpscmat  20695  chpscmatgsumbin  20697  chpscmatgsummon  20698  chfacfscmulcl  20710  cpmadugsumlemB  20727  cpmadugsumlemC  20728  chcoeffeqlem  20738  cldmreon  20946  neiptopreu  20985  maxlp  20999  ordttopon  21045  ordtrest2lem  21055  cnprcl2  21103  lmcnp  21156  resthauslem  21215  hauscmplem  21257  1stcfb  21296  2ndcctbss  21306  2ndcomap  21309  dis2ndc  21311  loclly  21338  hausllycmp  21345  locfincmp  21377  dissnref  21379  kgeni  21388  kgenidm  21398  ptpjpre2  21431  xkoopn  21440  txopn  21453  ptpjopn  21463  ptcldmpt  21465  ptcls  21467  pthaus  21489  txkgen  21503  xkohaus  21504  xkopt  21506  txconn  21540  imastps  21572  kqid  21579  kqopn  21585  kqcld  21586  isr0  21588  indishmph  21649  pt1hmeo  21657  ptuncnv  21658  ptunhmeo  21659  t0kq  21669  filconn  21734  uzrest  21748  uffixsn  21776  fmfnfmlem2  21806  flimss2  21823  flimss1  21824  flimclslem  21835  flfcnp  21855  fclsfnflim  21878  uffclsflim  21882  fcfelbas  21887  alexsublem  21895  alexsub  21896  cnextcn  21918  cnextfres1  21919  tmdgsum  21946  distgp  21950  indistgp  21951  symgtgp  21952  ghmcnp  21965  qustgpopn  21970  qustgplem  21971  qustgphaus  21973  prdstmdd  21974  prdstgpd  21975  tsmsid  21990  tsmssubm  21993  tsmsmhm  21996  tsmsadd  21997  tsmssplit  22002  utop2nei  22101  utop3cls  22102  neipcfilu  22147  cnextucn  22154  ucnextcn  22155  blpnfctr  22288  lpbl  22355  met2ndci  22374  tmsxps  22388  metcnpi  22396  metcnpi2  22397  metcnpi3  22398  metustid  22406  metustsym  22407  metustexhalf  22408  subgngp  22486  ngptgp  22487  sranlm  22535  nlmvscn  22538  nrginvrcn  22543  lssnlm  22552  nghmcn  22596  iccntr  22671  icccmplem2  22673  msdcn  22691  cncfmptc  22761  cncfmptid  22762  cncfmpt2f  22764  icoopnst  22785  iocopnst  22786  nmoleub2lem3  22961  nmoleub3  22965  nmhmcn  22966  ipcn  23091  cfilfcls  23118  caucfil  23127  equivcau  23144  caubl  23152  flimcfil  23158  rrxdstprj1  23238  minveclem3b  23245  minveclem4  23249  ovolicc2lem3  23333  ovolicc2lem4  23334  opnmbllem  23415  vitalilem2  23423  mbfsup  23476  mbfinf  23477  mbfi1fseqlem4  23530  limccnp  23700  limccnp2  23701  dvreslem  23718  dvres2lem  23719  dvidlem  23724  dvcnp2  23728  dvcn  23729  dvaddbr  23746  dvmulbr  23747  dvcmul  23752  dvcof  23756  dvcnvlem  23784  dvef  23788  rollelem  23797  dvlip2  23803  dvivthlem1  23816  dvivth  23818  lhop2  23823  lhop  23824  dvcnvrelem1  23825  dvcnvrelem2  23826  dvcnvre  23827  ply1rem  23968  fta1blem  23973  plycpn  24089  plyrem  24105  tayl0  24161  dvtaylp  24169  dvntaylp  24170  dvntaylp0  24171  taylthlem1  24172  taylthlem2  24173  ulmdvlem3  24201  psercn  24225  pserdv  24228  abelth  24240  efabl  24341  efopnlem1  24447  loglesqrt  24544  relogbf  24574  efrlim  24741  dchrghm  25026  dchrptlem3  25036  tgbtwntriv2  25427  tgbtwnne  25430  ercgrg  25457  tgidinside  25511  tgbtwnconn1  25515  tglnne  25568  tglnne0  25580  tglnpt2  25581  tglineneq  25584  ncolncol  25586  coltr3  25588  mirln  25616  mirln2  25617  mirconn  25618  krippenlem  25630  footex  25658  colperpexlem3  25669  mideulem2  25671  opphllem  25672  oppne3  25680  opphllem1  25684  opphllem2  25685  opphllem4  25687  oppperpex  25690  opphl  25691  hlpasch  25693  hpgerlem  25702  colhp  25707  midbtwn  25716  lmieu  25721  lmiisolem  25733  sacgr  25767  f1otrg  25796  f1otrge  25797  ebtwntg  25907  ecgrtg  25908  eengtrkg  25910  eengtrkge  25911  upgr1eop  26055  usgredg3  26153  uspgr1eop  26184  usgr1eop  26187  vtxdun  26433  vtxdfiun  26434  1loopgruspgr  26452  1loopgrvd2  26455  1hevtxdg1  26458  1egrvtxdg1  26461  1egrvtxdg0  26463  umgr2v2e  26477  wlkres  26623  wlkp1lem4  26629  wlkp1  26634  wwlksm1edg  26835  wwlksnext  26856  wwlksnextproplem3  26874  clwwlkel  27009  1wlkdlem2  27116  trlsegvdeg  27205  eupth2lem3lem1  27206  eupth2lem3lem2  27207  rspc2vd  27245  extwwlkfablem  27326  clwwlkccatlem  27331  extwwlkfab  27342  numclwlk2lem2f  27357  numclwlk2lem2fOLD  27364  spansnid  28550  elspansn4  28560  submarchi  29868  psgnfzto1stlem  29978  1smat1  29998  submat1n  29999  lmatfval  30008  lmatcl  30010  mdetpmtr1  30017  madjusmdetlem4  30024  qtopt1  30030  qtophaus  30031  locfinref  30036  ordtrest2NEWlem  30096  elzrhunit  30151  qqhcn  30163  qqhucn  30164  esumel  30237  esumsplit  30243  sigagenss2  30341  elsx  30385  sxbrsigalem0  30461  dya2icoseg  30467  eulerpartlemb  30558  eulerpartlemgvv  30566  iwrdsplit  30577  sseqfv2  30584  probfinmeasb  30619  dstrvprob  30661  dstfrvel  30663  ballotlemrv  30709  signstfvn  30774  signstfvp  30776  signstfveq0  30782  signsvtp  30788  signsvtn  30789  reprsuc  30821  reprpmtf1o  30832  bnj1006  31155  bnj1018  31158  bnj1121  31179  bnj1398  31228  bnj1450  31244  bnj1501  31261  subfacp1lem5  31292  ptpconn  31341  indispconn  31342  cvxsconn  31351  cvmseu  31384  cvmliftmolem2  31390  cvmliftlem7  31399  cvmliftlem10  31402  cvmliftlem13  31404  cvmlift2lem12  31422  mrsubcv  31533  mrsubff  31535  mrsubrn  31536  mrsubccat  31541  elmrsubrn  31543  mrsubco  31544  mrsubvrs  31545  mvhf  31581  msubvrs  31583  mclsax  31592  frrlem11  31917  nodenselem5  31963  nosupres  31978  linerflx1  32381  linerflx2  32383  fwddifnval  32395  elhf2  32407  neibastop2lem  32480  icoreunrn  33337  relowlssretop  33341  sucneqond  33343  matunitlindflem2  33536  poimirlem4  33543  poimirlem20  33559  poimirlem30  33569  broucube  33573  opnmbllem0  33575  areacirclem2  33631  areacirclem4  33633  blssp  33682  sstotbnd2  33703  totbndbnd  33718  prdstotbnd  33723  cnpwstotbnd  33726  heiborlem9  33748  exidcl  33805  exidresid  33808  grpokerinj  33822  iscringd  33927  prter3  34486  toycom  34578  islfld  34667  lshpsmreu  34714  ldualelvbase  34732  ldualssvscl  34763  lkreqN  34775  lkrlspeqN  34776  erng1lem  36592  erngdvlem4  36596  erng0g  36599  erng1r  36600  erngdvlem4-rN  36604  dva0g  36633  dia1dim2  36668  dia1dimid  36669  dia2dimlem5  36674  dvhelvbasei  36694  dvhvaddass  36703  tendoinvcl  36710  tendolinv  36711  tendorinv  36712  dvhgrp  36713  dvhlveclem  36714  cdlemn4  36804  lcfrlem12N  37160  lcfrlem15  37163  lcdvscl  37211  lcdlssvscl  37212  lcdvsass  37213  lcdvs0N  37222  mapdincl  37267  mapdin  37268  mapdlsmcl  37269  mapdcnvatN  37272  mapdpglem2  37279  mapdpglem12  37289  mapdpglem18  37295  mapdpglem21  37298  mapdpglem22  37299  mapdpglem28  37307  mapdpglem30  37308  hdmaprnlem3N  37459  hdmaprnlem3uN  37460  hdmaprnlem7N  37464  hdmaprnlem8N  37465  hdmaprnlem9N  37466  hdmaprnlem3eN  37467  hdmaprnlem16N  37471  hgmapdcl  37499  hgmapval1  37502  hgmaprnlem4N  37508  hdmapinvlem1  37527  wepwsolem  37929  kercvrlsm  37970  dfacbasgrp  37995  cntzsdrg  38089  imo72b2lem0  38782  dvconstbi  38850  cncmpmax  39505  iooabslt  40039  fmul01lt1lem2  40135  limciccioolb  40171  limcicciooub  40187  limsuppnfdlem  40251  climrescn  40298  climxrrelem  40299  climxrre  40300  xlimmnfvlem2  40377  xlimpnfvlem2  40381  fsumcncf  40409  ioccncflimc  40416  icocncflimc  40420  cncfiooicclem1  40424  dvbdfbdioolem2  40462  dvnmul  40476  stoweidlem26  40561  stoweidlem34  40569  stoweidlem48  40583  stoweidlem59  40594  dirkercncflem3  40640  fourierdlem32  40674  fourierdlem41  40683  fourierdlem51  40692  fourierdlem63  40704  fourierdlem82  40723  fourierdlem85  40726  fourierdlem93  40734  fourierdlem111  40752  fourierdlem114  40755  etransclem35  40804  hspdifhsp  41151  opnvonmbllem1  41167  ovnovollem1  41191  mbfresmf  41269  smfaddlem1  41292  smfsuplem1  41338  smflimsuplem5  41351  fzoopth  41662  setsidel  41671  setsnidel  41672  pfxccat1  41735  pfxccatin12  41750  repswpfx  41761  prelspr  42061  rnghmsubcsetclem1  42300  rngccatidALTV  42314  zrinitorngc  42325  zrtermorngc  42326  zrzeroorngc  42327  rhmsubcsetclem1  42346  rhmsubcrngclem1  42352  funcringcsetcALTV2lem3  42363  funcringcsetcALTV2lem8  42368  ringccatidALTV  42377  funcringcsetclem3ALTV  42386  funcringcsetclem8ALTV  42391  irinitoringc  42394  zrtermoringc  42395  zrninitoringc  42396  nzerooringczr  42397  srhmsubclem2  42399  srhmsubc  42401  srhmsubcALTVlem1  42417  srhmsubcALTV  42419  rhmsubcALTVlem3  42431  lcosslsp  42552  nnolog2flm1  42709
  Copyright terms: Public domain W3C validator