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

Theorem eleqtrrd 2916
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 2827 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrd 2915 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893
This theorem is referenced by:  3eltr4d  2928  rspc2vd  3931  disjxiun  5055  eldmressnsn  5889  elimdelov  7239  elovmpt3rab1  7394  fnwelem  7816  tfrlem13  8017  tz7.44-2  8034  omordi  8182  oneo  8197  omeulem2  8199  oeordi  8203  oeeui  8218  nnneo  8268  erref  8299  en1uniel  8570  omxpenlem  8607  unblem3  8761  dffi3  8884  ordtypelem10  8980  oismo  8993  cantnff  9126  cantnfp1lem3  9132  cantnflem1  9141  cnfcom  9152  r1ordg  9196  r1pwss  9202  rankwflemb  9211  r1elwf  9214  rankidb  9218  rankonidlem  9246  fseqenlem2  9440  dfac12lem1  9558  dfac12lem2  9559  pwsdompw  9615  ackbij2lem3  9652  ackbij2  9654  cfsmolem  9681  hsmexlem4  9840  ttukeylem3  9922  ttukeylem7  9926  iundom2g  9951  fpwwe2lem9  10049  canthwelem  10061  pwfseqlem4  10073  winalim2  10107  r1wunlim  10148  tskmid  10251  fzopth  12934  predfz  13022  fzoss2  13055  fz1fzo0m1  13075  fzo0addel  13081  fzo0addelr  13082  fzosubel3  13088  elfzomin  13099  elfzonlteqm1  13103  fzoend  13118  fzofzp1  13124  fzofzp1b  13125  peano2fzor  13134  zmodfzo  13252  seqf1olem2  13400  bcn2  13669  swrdccat2  14021  pfxccat1  14054  swrdswrd  14057  pfxccatin12  14085  splfv1  14107  revcl  14113  revlen  14114  revccat  14118  revrev  14119  repswpfx  14137  cshwidxmod  14155  revco  14186  limsupgre  14828  summolem2a  15062  fsumm1  15096  fsumcom2  15119  prodmolem2a  15278  fprodm1  15311  fprodcom2  15328  prmreclem4  16245  prmreclem5  16246  vdwapid1  16301  vdwlem5  16311  vdwlem8  16314  vdwnnlem2  16322  ramub1lem1  16352  ramub1lem2  16353  mrieqvlemd  16890  mreexd  16903  mreexexlemd  16905  catcocl  16946  catass  16947  moni  16996  epii  17003  inviso1  17026  episect  17045  invisoinvl  17050  catsubcat  17099  subccocl  17105  fullsubc  17110  funcco  17131  resf2nd  17155  funcres  17156  fthepi  17188  nati  17215  arwhoma  17295  catccatid  17352  resscatc  17355  catcisolem  17356  catcoppccl  17358  catcfuccl  17359  estrreslem2  17378  funcestrcsetclem3  17382  funcestrcsetclem8  17387  equivestrcsetc  17392  funcsetcestrclem3  17396  funcsetcestrclem8  17402  xpcco  17423  xpcco2  17427  xpccatid  17428  prfcl  17443  catcxpccl  17447  curf12  17467  curf1cl  17468  curf2  17469  curf2cl  17471  curfcl  17472  uncf2  17477  uncfcurf  17479  diag12  17484  diag2  17485  curf2ndf  17487  hofcl  17499  oppchofcl  17500  oyoncl  17510  yonedalem3a  17514  yonedalem4b  17516  yonedalem22  17518  yonedalem3b  17519  yonedalem3  17520  yonedainv  17521  yonffthlem  17522  latcl2  17648  latlem  17649  latjcom  17659  latmcom  17675  clatlem  17711  clatlubcl2  17713  clatglbcl2  17715  acsfiindd  17777  gsumpropd2lem  17879  mndpropd  17926  imasmnd  17939  frmdmnd  18014  frmdgsum  18017  grpsubpropd2  18145  imasgrp  18155  subg0  18225  0ghm  18312  resghm2  18315  ghmco  18318  pwsdiagghm  18326  psgnunilem1  18552  psgnunilem5  18553  psgnunilem2  18554  psgnunilem3  18555  sylow1lem4  18657  sylow1lem5  18658  efglem  18773  efgtf  18779  efginvrel2  18784  efginvrel1  18785  efgsdmi  18789  efgs1b  18793  efgsres  18795  efgsfo  18796  efgredleme  18800  efgredlemc  18802  efgredlem  18804  efgcpbllemb  18812  frgp0  18817  frgpadd  18820  frgpinv  18821  vrgpf  18825  vrgpinv  18826  frgpuplem  18829  frgpup1  18832  frgpup2  18833  frgpup3lem  18834  frgpnabllem1  18924  frgpnabllem2  18925  gsumval3  18958  dprdfid  19070  dprdsn  19089  dprd2da  19095  dpjidcl  19111  pgpfac1lem2  19128  pgpfaclem3  19136  ablsimpg1gend  19158  ablsimpgprmd  19168  ringpropd  19263  imasring  19300  qusring2  19301  pwsco1rhm  19421  pwsco2rhm  19422  subrgunit  19484  pwsdiagrhm  19500  cntzsdrg  19512  isabvd  19522  lmodprop2d  19627  islssd  19638  prdsvscacl  19671  prdslmodd  19672  islmhm2  19741  lmhmco  19746  lmhmplusg  19747  lmhmvsca  19748  lmhmpropd  19776  lsppreli  19793  lspsnel4  19827  lssacsex  19847  lspsnat  19848  qus1  19938  qusrhm  19940  assapropd  20031  psr0cl  20104  psrnegcl  20106  psr1cl  20112  resspsrmul  20127  subrgpsr  20129  mvrf  20134  mplmon  20174  mplcoe1  20176  subrgasclcl  20209  mplind  20212  evlslem1  20225  subrgply1  20331  psrplusgpropd  20334  ply1coe  20394  cply1coe0bi  20398  lply1binomsc  20405  evls1val  20413  evls1rhm  20415  evl1val  20422  evl1rhm  20425  pf1ind  20448  evl1scvarpw  20456  znf1o  20628  cssmre  20767  dsmmlss  20818  frlmsplit2  20847  frlmbas3  20850  frlmup1  20872  matbas2i  20961  matplusg2  20966  matvsca2  20967  matsubgcell  20973  matvscacell  20975  mpomatmul  20985  mavmulval  21084  mavmulcl  21086  mavmulass  21088  mavmul0  21091  mavmumamul1  21094  m1detdiag  21136  cramerimplem2  21223  mat2pmatmul  21269  mat2pmatlin  21273  monmatcollpw  21317  pmatcollpwfi  21320  mply1topmatcl  21343  pm2mpghm  21354  pm2mpmhmlem2  21357  pm2mp  21363  chpmat1dlem  21373  chpmat1d  21374  chpdmatlem0  21375  chpscmat  21380  chpscmatgsumbin  21382  chpscmatgsummon  21383  chfacfscmulcl  21395  cpmadugsumlemB  21412  cpmadugsumlemC  21413  chcoeffeqlem  21423  cldmreon  21632  neiptopreu  21671  maxlp  21685  ordttopon  21731  ordtrest2lem  21741  cnprcl2  21789  lmcnp  21842  resthauslem  21901  hauscmplem  21944  1stcfb  21983  2ndcctbss  21993  2ndcomap  21996  dis2ndc  21998  loclly  22025  hausllycmp  22032  locfincmp  22064  dissnref  22066  kgeni  22075  kgenidm  22085  ptpjpre2  22118  xkoopn  22127  txopn  22140  ptpjopn  22150  ptcldmpt  22152  ptcls  22154  pthaus  22176  txkgen  22190  xkohaus  22191  xkopt  22193  txconn  22227  imastps  22259  kqid  22266  kqopn  22272  kqcld  22273  isr0  22275  indishmph  22336  pt1hmeo  22344  ptuncnv  22345  ptunhmeo  22346  t0kq  22356  filconn  22421  uzrest  22435  uffixsn  22463  fmfnfmlem2  22493  flimss2  22510  flimss1  22511  flimclslem  22522  flfcnp  22542  fclsfnflim  22565  uffclsflim  22569  fcfelbas  22574  alexsublem  22582  alexsub  22583  cnextcn  22605  cnextfres1  22606  cnextfres  22607  tmdgsum  22633  distgp  22637  indistgp  22638  symgtgp  22639  ghmcnp  22652  qustgpopn  22657  qustgplem  22658  qustgphaus  22660  prdstmdd  22661  prdstgpd  22662  tsmsid  22677  tsmssubm  22680  tsmsmhm  22683  tsmsadd  22684  tsmssplit  22689  utop2nei  22788  utop3cls  22789  neipcfilu  22834  cnextucn  22841  ucnextcn  22842  blpnfctr  22975  lpbl  23042  met2ndci  23061  tmsxps  23075  metcnpi  23083  metcnpi2  23084  metcnpi3  23085  metustid  23093  metustsym  23094  metustexhalf  23095  subgngp  23173  ngptgp  23174  sranlm  23222  nlmvscn  23225  nrginvrcn  23230  lssnlm  23239  nghmcn  23283  iccntr  23358  icccmplem2  23360  msdcn  23378  cncfmptc  23448  cncfmptid  23449  cncfmpt2f  23451  icoopnst  23472  iocopnst  23473  nmoleub2lem3  23648  nmoleub3  23652  nmhmcn  23653  ipcn  23778  cfilfcls  23806  caucfil  23815  equivcau  23832  caubl  23840  flimcfil  23846  cmssmscld  23882  rrxdstprj1  23941  minveclem3b  23960  minveclem4  23964  ovolicc2lem3  24049  ovolicc2lem4  24050  opnmbllem  24131  vitalilem2  24139  mbfsup  24194  mbfinf  24195  mbfi1fseqlem4  24248  limccnp  24418  limccnp2  24419  dvreslem  24436  dvres2lem  24437  dvidlem  24442  dvcnp2  24446  dvcn  24447  dvaddbr  24464  dvmulbr  24465  dvcmul  24470  dvcof  24474  dvcnvlem  24502  dvef  24506  rollelem  24515  dvlip2  24521  dvivthlem1  24534  dvivth  24536  lhop2  24541  lhop  24542  dvcnvrelem1  24543  dvcnvrelem2  24544  dvcnvre  24545  ply1rem  24686  fta1blem  24691  plycpn  24807  plyrem  24823  tayl0  24879  dvtaylp  24887  dvntaylp  24888  dvntaylp0  24889  taylthlem1  24890  taylthlem2  24891  ulmdvlem3  24919  psercn  24943  pserdv  24946  abelth  24958  efabl  25061  efopnlem1  25166  loglesqrt  25266  relogbf  25296  efrlim  25475  dchrghm  25760  dchrptlem3  25770  tgbtwntriv2  26201  tgbtwnne  26204  ercgrg  26231  tgidinside  26285  tgbtwnconn1  26289  tglnne  26342  tglnne0  26354  tglnpt2  26355  tglineneq  26358  ncolncol  26360  coltr3  26362  mirln  26390  mirln2  26391  mirconn  26392  krippenlem  26404  footexALT  26432  footexlem1  26433  footexlem2  26434  colperpexlem3  26446  mideulem2  26448  opphllem  26449  oppne3  26457  opphllem1  26461  opphllem2  26462  opphllem4  26464  oppperpex  26467  opphl  26468  hlpasch  26470  hpgerlem  26479  colhp  26484  midbtwn  26493  lmieu  26498  lmiisolem  26510  sacgr  26545  f1otrg  26585  f1otrge  26586  ebtwntg  26696  ecgrtg  26697  eengtrkg  26700  eengtrkge  26701  upgr1eop  26828  usgredg3  26926  uspgr1eop  26957  usgr1eop  26960  vtxdun  27191  vtxdfiun  27192  1loopgruspgr  27210  1loopgrvd2  27213  1hevtxdg1  27216  1egrvtxdg1  27219  1egrvtxdg0  27221  umgr2v2e  27235  wlkres  27380  wlkp1lem4  27386  wlkp1  27391  wwlksm1edg  27587  wwlksnext  27599  wwlksnextproplem3  27618  clwwlkel  27753  1wlkdlem2  27845  trlsegvdeg  27934  eupth2lem3lem1  27935  eupth2lem3lem2  27936  extwwlkfab  28059  numclwlk2lem2f  28084  spansnid  29268  elspansn4  29278  fnpreimac  30345  ccatf1  30553  swrdrn2  30556  swrdrn3  30557  swrdf1  30558  splfv3  30560  psgnfzto1stlem  30670  cycpmfv1  30683  cycpmfv2  30684  cycpmco2lem2  30697  cycpmco2lem4  30699  cycpmco2lem5  30700  cycpmco2lem6  30701  cycpmco2  30703  cyc3co2  30710  cycpmrn  30713  submarchi  30743  imaslmod  30850  quslmod  30851  quslmhm  30852  fply1  30859  lidlnsg  30880  qsidomlem2  30884  drgextlsp  30896  matdim  30913  lindsunlem  30920  qusdimsum  30924  fedgmullem1  30925  fedgmullem2  30926  fedgmul  30927  extdg1id  30953  1smat1  30969  submat1n  30970  lmatfval  30979  lmatcl  30981  mdetpmtr1  30988  madjusmdetlem4  30995  qtopt1  30999  qtophaus  31000  locfinref  31005  ordtrest2NEWlem  31065  elzrhunit  31120  qqhcn  31132  qqhucn  31133  esumel  31206  esumsplit  31212  sigagenss2  31309  elsx  31353  sxbrsigalem0  31429  dya2icoseg  31435  eulerpartlemb  31526  eulerpartlemgvv  31534  iwrdsplit  31545  sseqfv2  31552  probfinmeasb  31586  dstrvprob  31629  dstfrvel  31631  ballotlemrv  31677  signstfvn  31739  signstfvp  31741  signstfveq0  31747  signsvtp  31753  signsvtn  31754  reprsuc  31786  reprpmtf1o  31797  lpadleft  31854  bnj1006  32131  bnj1018  32134  bnj1121  32155  bnj1398  32204  bnj1450  32220  bnj1501  32237  revpfxsfxrev  32260  swrdrevpfx  32261  pfxwlk  32268  revwlk  32269  swrdwlk  32271  subfacp1lem5  32329  ptpconn  32378  indispconn  32379  cvxsconn  32388  cvmseu  32421  cvmliftmolem2  32427  cvmliftlem7  32436  cvmliftlem10  32439  cvmliftlem13  32441  cvmlift2lem12  32459  satfv1lem  32507  satffunlem1lem2  32548  satffunlem2lem2  32551  satefvfmla1  32570  mrsubcv  32655  mrsubff  32657  mrsubrn  32658  mrsubccat  32663  elmrsubrn  32665  mrsubco  32666  mrsubvrs  32667  mvhf  32703  msubvrs  32705  mclsax  32714  nodenselem5  33090  nosupres  33105  linerflx1  33508  linerflx2  33510  fwddifnval  33522  elhf2  33534  neibastop2lem  33606  icoreunrn  34523  relowlssretop  34527  sucneqond  34529  matunitlindflem2  34771  poimirlem4  34778  poimirlem20  34794  poimirlem30  34804  broucube  34808  opnmbllem0  34810  areacirclem2  34865  areacirclem4  34867  blssp  34914  sstotbnd2  34935  totbndbnd  34950  prdstotbnd  34955  cnpwstotbnd  34958  heiborlem9  34980  exidcl  35037  exidresid  35040  grpokerinj  35054  iscringd  35159  erim2  35793  prter3  35900  toycom  35991  islfld  36080  lshpsmreu  36127  ldualelvbase  36145  ldualssvscl  36176  lkreqN  36188  lkrlspeqN  36189  erng1lem  38005  erngdvlem4  38009  erng0g  38012  erng1r  38013  erngdvlem4-rN  38017  dva0g  38045  dia1dim2  38080  dia1dimid  38081  dia2dimlem5  38086  dvhelvbasei  38106  dvhvaddass  38115  tendoinvcl  38122  tendolinv  38123  tendorinv  38124  dvhgrp  38125  dvhlveclem  38126  cdlemn4  38216  lcfrlem12N  38572  lcfrlem15  38575  lcdvscl  38623  lcdlssvscl  38624  lcdvsass  38625  lcdvs0N  38634  mapdincl  38679  mapdin  38680  mapdlsmcl  38681  mapdcnvatN  38684  mapdpglem2  38691  mapdpglem12  38701  mapdpglem18  38707  mapdpglem21  38710  mapdpglem22  38711  mapdpglem28  38719  mapdpglem30  38720  hdmaprnlem3N  38868  hdmaprnlem3uN  38869  hdmaprnlem7N  38873  hdmaprnlem8N  38874  hdmaprnlem9N  38875  hdmaprnlem3eN  38876  hdmaprnlem16N  38880  hgmapdcl  38908  hgmapval1  38911  hgmaprnlem4N  38917  hdmapinvlem1  38936  fnsnbt  39000  selvval2lem2  39013  selvval2lem4  39016  fltnltalem  39154  wepwsolem  39522  kercvrlsm  39563  dfacbasgrp  39588  imo72b2lem0  40396  grurankcld  40449  grumnudlem  40501  grumnud  40502  inaex  40513  gruex  40514  dvconstbi  40546  cncmpmax  41169  iooabslt  41654  fmul01lt1lem2  41746  limciccioolb  41782  limcicciooub  41798  limsuppnfdlem  41862  climrescn  41909  climxrrelem  41910  climxrre  41911  liminflimsupxrre  41978  xlimmnfvlem2  41994  xlimpnfvlem2  41998  fsumcncf  42041  ioccncflimc  42048  icocncflimc  42052  cncfiooicclem1  42056  dvbdfbdioolem2  42094  dvnmul  42108  stoweidlem26  42192  stoweidlem34  42200  stoweidlem48  42214  stoweidlem59  42225  dirkercncflem3  42271  fourierdlem32  42305  fourierdlem41  42314  fourierdlem51  42323  fourierdlem63  42335  fourierdlem82  42354  fourierdlem85  42357  fourierdlem93  42365  fourierdlem111  42383  fourierdlem114  42386  etransclem35  42435  hspdifhsp  42779  opnvonmbllem1  42795  ovnovollem1  42819  mbfresmf  42897  smfaddlem1  42920  smfsuplem1  42966  smflimsuplem5  42979  fzoopth  43408  setsidel  43417  setsnidel  43418  prelspr  43495  rnghmsubcsetclem1  44144  rngccatidALTV  44158  zrinitorngc  44169  zrtermorngc  44170  zrzeroorngc  44171  rhmsubcsetclem1  44190  rhmsubcrngclem1  44196  funcringcsetcALTV2lem3  44207  funcringcsetcALTV2lem8  44212  ringccatidALTV  44221  funcringcsetclem3ALTV  44230  funcringcsetclem8ALTV  44235  irinitoringc  44238  zrtermoringc  44239  zrninitoringc  44240  nzerooringczr  44241  srhmsubclem2  44243  srhmsubc  44245  srhmsubcALTVlem1  44261  srhmsubcALTV  44263  rhmsubcALTVlem3  44275  lcosslsp  44391  nnolog2flm1  44548
  Copyright terms: Public domain W3C validator