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

Theorem eleqtrrd 2913
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 2824 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrd 2912 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 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890
This theorem is referenced by:  3eltr4d  2925  rspc2vd  3929  disjxiun  5054  eldmressnsn  5888  elimdelov  7239  elovmpt3rab1  7394  fnwelem  7814  tfrlem13  8015  tz7.44-2  8032  omordi  8181  oneo  8196  omeulem2  8198  oeordi  8202  oeeui  8217  nnneo  8267  erref  8298  en1uniel  8569  omxpenlem  8606  unblem3  8760  dffi3  8883  ordtypelem10  8979  oismo  8992  cantnff  9125  cantnfp1lem3  9131  cantnflem1  9140  cnfcom  9151  r1ordg  9195  r1pwss  9201  rankwflemb  9210  r1elwf  9213  rankidb  9217  rankonidlem  9245  fseqenlem2  9439  dfac12lem1  9557  dfac12lem2  9558  pwsdompw  9614  ackbij2lem3  9651  ackbij2  9653  cfsmolem  9680  hsmexlem4  9839  ttukeylem3  9921  ttukeylem7  9925  iundom2g  9950  fpwwe2lem9  10048  canthwelem  10060  pwfseqlem4  10072  winalim2  10106  r1wunlim  10147  tskmid  10250  fzopth  12932  predfz  13020  fzoss2  13053  fz1fzo0m1  13073  fzo0addel  13079  fzo0addelr  13080  fzosubel3  13086  elfzomin  13097  elfzonlteqm1  13101  fzoend  13116  fzofzp1  13122  fzofzp1b  13123  peano2fzor  13132  zmodfzo  13250  seqf1olem2  13398  bcn2  13667  swrdccat2  14019  pfxccat1  14052  swrdswrd  14055  pfxccatin12  14083  splfv1  14105  revcl  14111  revlen  14112  revccat  14116  revrev  14117  repswpfx  14135  cshwidxmod  14153  revco  14184  limsupgre  14826  summolem2a  15060  fsumm1  15094  fsumcom2  15117  prodmolem2a  15276  fprodm1  15309  fprodcom2  15326  prmreclem4  16243  prmreclem5  16244  vdwapid1  16299  vdwlem5  16309  vdwlem8  16312  vdwnnlem2  16320  ramub1lem1  16350  ramub1lem2  16351  mrieqvlemd  16888  mreexd  16901  mreexexlemd  16903  catcocl  16944  catass  16945  moni  16994  epii  17001  inviso1  17024  episect  17043  invisoinvl  17048  catsubcat  17097  subccocl  17103  fullsubc  17108  funcco  17129  resf2nd  17153  funcres  17154  fthepi  17186  nati  17213  arwhoma  17293  catccatid  17350  resscatc  17353  catcisolem  17354  catcoppccl  17356  catcfuccl  17357  estrreslem2  17376  funcestrcsetclem3  17380  funcestrcsetclem8  17385  equivestrcsetc  17390  funcsetcestrclem3  17394  funcsetcestrclem8  17400  xpcco  17421  xpcco2  17425  xpccatid  17426  prfcl  17441  catcxpccl  17445  curf12  17465  curf1cl  17466  curf2  17467  curf2cl  17469  curfcl  17470  uncf2  17475  uncfcurf  17477  diag12  17482  diag2  17483  curf2ndf  17485  hofcl  17497  oppchofcl  17498  oyoncl  17508  yonedalem3a  17512  yonedalem4b  17514  yonedalem22  17516  yonedalem3b  17517  yonedalem3  17518  yonedainv  17519  yonffthlem  17520  latcl2  17646  latlem  17647  latjcom  17657  latmcom  17673  clatlem  17709  clatlubcl2  17711  clatglbcl2  17713  acsfiindd  17775  gsumpropd2lem  17877  mndpropd  17924  imasmnd  17937  frmdmnd  18012  frmdgsum  18015  grpsubpropd2  18143  imasgrp  18153  subg0  18223  0ghm  18310  resghm2  18313  ghmco  18316  pwsdiagghm  18324  psgnunilem1  18550  psgnunilem5  18551  psgnunilem2  18552  psgnunilem3  18553  sylow1lem4  18655  sylow1lem5  18656  efglem  18771  efgtf  18777  efginvrel2  18782  efginvrel1  18783  efgsdmi  18787  efgs1b  18791  efgsres  18793  efgsfo  18794  efgredleme  18798  efgredlemc  18800  efgredlem  18802  efgcpbllemb  18810  frgp0  18815  frgpadd  18818  frgpinv  18819  vrgpf  18823  vrgpinv  18824  frgpuplem  18827  frgpup1  18830  frgpup2  18831  frgpup3lem  18832  frgpnabllem1  18922  frgpnabllem2  18923  gsumval3  18956  dprdfid  19068  dprdsn  19087  dprd2da  19093  dpjidcl  19109  pgpfac1lem2  19126  pgpfaclem3  19134  ablsimpg1gend  19156  ablsimpgprmd  19166  ringpropd  19261  imasring  19298  qusring2  19299  pwsco1rhm  19419  pwsco2rhm  19420  subrgunit  19482  pwsdiagrhm  19498  cntzsdrg  19510  isabvd  19520  lmodprop2d  19625  islssd  19636  prdsvscacl  19669  prdslmodd  19670  islmhm2  19739  lmhmco  19744  lmhmplusg  19745  lmhmvsca  19746  lmhmpropd  19774  lsppreli  19791  lspsnel4  19825  lssacsex  19845  lspsnat  19846  qus1  19936  qusrhm  19938  assapropd  20029  psr0cl  20102  psrnegcl  20104  psr1cl  20110  resspsrmul  20125  subrgpsr  20127  mvrf  20132  mplmon  20172  mplcoe1  20174  subrgasclcl  20207  mplind  20210  evlslem1  20223  subrgply1  20329  psrplusgpropd  20332  ply1coe  20392  cply1coe0bi  20396  lply1binomsc  20403  evls1val  20411  evls1rhm  20413  evl1val  20420  evl1rhm  20423  pf1ind  20446  evl1scvarpw  20454  znf1o  20626  cssmre  20765  dsmmlss  20816  frlmsplit2  20845  frlmbas3  20848  frlmup1  20870  matbas2i  20959  matplusg2  20964  matvsca2  20965  matsubgcell  20971  matvscacell  20973  mpomatmul  20983  mavmulval  21082  mavmulcl  21084  mavmulass  21086  mavmul0  21089  mavmumamul1  21092  m1detdiag  21134  cramerimplem2  21221  mat2pmatmul  21267  mat2pmatlin  21271  monmatcollpw  21315  pmatcollpwfi  21318  mply1topmatcl  21341  pm2mpghm  21352  pm2mpmhmlem2  21355  pm2mp  21361  chpmat1dlem  21371  chpmat1d  21372  chpdmatlem0  21373  chpscmat  21378  chpscmatgsumbin  21380  chpscmatgsummon  21381  chfacfscmulcl  21393  cpmadugsumlemB  21410  cpmadugsumlemC  21411  chcoeffeqlem  21421  cldmreon  21630  neiptopreu  21669  maxlp  21683  ordttopon  21729  ordtrest2lem  21739  cnprcl2  21787  lmcnp  21840  resthauslem  21899  hauscmplem  21942  1stcfb  21981  2ndcctbss  21991  2ndcomap  21994  dis2ndc  21996  loclly  22023  hausllycmp  22030  locfincmp  22062  dissnref  22064  kgeni  22073  kgenidm  22083  ptpjpre2  22116  xkoopn  22125  txopn  22138  ptpjopn  22148  ptcldmpt  22150  ptcls  22152  pthaus  22174  txkgen  22188  xkohaus  22189  xkopt  22191  txconn  22225  imastps  22257  kqid  22264  kqopn  22270  kqcld  22271  isr0  22273  indishmph  22334  pt1hmeo  22342  ptuncnv  22343  ptunhmeo  22344  t0kq  22354  filconn  22419  uzrest  22433  uffixsn  22461  fmfnfmlem2  22491  flimss2  22508  flimss1  22509  flimclslem  22520  flfcnp  22540  fclsfnflim  22563  uffclsflim  22567  fcfelbas  22572  alexsublem  22580  alexsub  22581  cnextcn  22603  cnextfres1  22604  cnextfres  22605  tmdgsum  22631  distgp  22635  indistgp  22636  symgtgp  22637  ghmcnp  22650  qustgpopn  22655  qustgplem  22656  qustgphaus  22658  prdstmdd  22659  prdstgpd  22660  tsmsid  22675  tsmssubm  22678  tsmsmhm  22681  tsmsadd  22682  tsmssplit  22687  utop2nei  22786  utop3cls  22787  neipcfilu  22832  cnextucn  22839  ucnextcn  22840  blpnfctr  22973  lpbl  23040  met2ndci  23059  tmsxps  23073  metcnpi  23081  metcnpi2  23082  metcnpi3  23083  metustid  23091  metustsym  23092  metustexhalf  23093  subgngp  23171  ngptgp  23172  sranlm  23220  nlmvscn  23223  nrginvrcn  23228  lssnlm  23237  nghmcn  23281  iccntr  23356  icccmplem2  23358  msdcn  23376  cncfmptc  23446  cncfmptid  23447  cncfmpt2f  23449  icoopnst  23470  iocopnst  23471  nmoleub2lem3  23646  nmoleub3  23650  nmhmcn  23651  ipcn  23776  cfilfcls  23804  caucfil  23813  equivcau  23830  caubl  23838  flimcfil  23844  cmssmscld  23880  rrxdstprj1  23939  minveclem3b  23958  minveclem4  23962  ovolicc2lem3  24047  ovolicc2lem4  24048  opnmbllem  24129  vitalilem2  24137  mbfsup  24192  mbfinf  24193  mbfi1fseqlem4  24246  limccnp  24416  limccnp2  24417  dvreslem  24434  dvres2lem  24435  dvidlem  24440  dvcnp2  24444  dvcn  24445  dvaddbr  24462  dvmulbr  24463  dvcmul  24468  dvcof  24472  dvcnvlem  24500  dvef  24504  rollelem  24513  dvlip2  24519  dvivthlem1  24532  dvivth  24534  lhop2  24539  lhop  24540  dvcnvrelem1  24541  dvcnvrelem2  24542  dvcnvre  24543  ply1rem  24684  fta1blem  24689  plycpn  24805  plyrem  24821  tayl0  24877  dvtaylp  24885  dvntaylp  24886  dvntaylp0  24887  taylthlem1  24888  taylthlem2  24889  ulmdvlem3  24917  psercn  24941  pserdv  24944  abelth  24956  efabl  25061  efopnlem1  25166  loglesqrt  25266  relogbf  25296  efrlim  25474  dchrghm  25759  dchrptlem3  25769  tgbtwntriv2  26200  tgbtwnne  26203  ercgrg  26230  tgidinside  26284  tgbtwnconn1  26288  tglnne  26341  tglnne0  26353  tglnpt2  26354  tglineneq  26357  ncolncol  26359  coltr3  26361  mirln  26389  mirln2  26390  mirconn  26391  krippenlem  26403  footexALT  26431  footexlem1  26432  footexlem2  26433  colperpexlem3  26445  mideulem2  26447  opphllem  26448  oppne3  26456  opphllem1  26460  opphllem2  26461  opphllem4  26463  oppperpex  26466  opphl  26467  hlpasch  26469  hpgerlem  26478  colhp  26483  midbtwn  26492  lmieu  26497  lmiisolem  26509  sacgr  26544  f1otrg  26584  f1otrge  26585  ebtwntg  26695  ecgrtg  26696  eengtrkg  26699  eengtrkge  26700  upgr1eop  26827  usgredg3  26925  uspgr1eop  26956  usgr1eop  26959  vtxdun  27190  vtxdfiun  27191  1loopgruspgr  27209  1loopgrvd2  27212  1hevtxdg1  27215  1egrvtxdg1  27218  1egrvtxdg0  27220  umgr2v2e  27234  wlkres  27379  wlkp1lem4  27385  wlkp1  27390  wwlksm1edg  27586  wwlksnext  27598  wwlksnextproplem3  27617  clwwlkel  27752  1wlkdlem2  27844  trlsegvdeg  27933  eupth2lem3lem1  27934  eupth2lem3lem2  27935  extwwlkfab  28058  numclwlk2lem2f  28083  spansnid  29267  elspansn4  29277  fnpreimac  30344  ccatf1  30552  swrdrn2  30555  swrdrn3  30556  swrdf1  30557  splfv3  30559  psgnfzto1stlem  30669  cycpmfv1  30682  cycpmfv2  30683  cycpmco2lem2  30696  cycpmco2lem4  30698  cycpmco2lem5  30699  cycpmco2lem6  30700  cycpmco2  30702  cyc3co2  30709  cycpmrn  30712  submarchi  30742  imaslmod  30849  quslmod  30850  quslmhm  30851  fply1  30858  lidlnsg  30879  qsidomlem2  30883  drgextlsp  30895  matdim  30912  lindsunlem  30919  qusdimsum  30923  fedgmullem1  30924  fedgmullem2  30925  fedgmul  30926  extdg1id  30952  1smat1  30968  submat1n  30969  lmatfval  30978  lmatcl  30980  mdetpmtr1  30987  madjusmdetlem4  30994  qtopt1  30998  qtophaus  30999  locfinref  31004  ordtrest2NEWlem  31064  elzrhunit  31119  qqhcn  31131  qqhucn  31132  esumel  31205  esumsplit  31211  sigagenss2  31308  elsx  31352  sxbrsigalem0  31428  dya2icoseg  31434  eulerpartlemb  31525  eulerpartlemgvv  31533  iwrdsplit  31544  sseqfv2  31551  probfinmeasb  31585  dstrvprob  31628  dstfrvel  31630  ballotlemrv  31676  signstfvn  31738  signstfvp  31740  signstfveq0  31746  signsvtp  31752  signsvtn  31753  reprsuc  31785  reprpmtf1o  31796  lpadleft  31853  bnj1006  32130  bnj1018  32133  bnj1121  32154  bnj1398  32203  bnj1450  32219  bnj1501  32236  revpfxsfxrev  32259  swrdrevpfx  32260  pfxwlk  32267  revwlk  32268  swrdwlk  32270  subfacp1lem5  32328  ptpconn  32377  indispconn  32378  cvxsconn  32387  cvmseu  32420  cvmliftmolem2  32426  cvmliftlem7  32435  cvmliftlem10  32438  cvmliftlem13  32440  cvmlift2lem12  32458  satfv1lem  32506  satffunlem1lem2  32547  satffunlem2lem2  32550  satefvfmla1  32569  mrsubcv  32654  mrsubff  32656  mrsubrn  32657  mrsubccat  32662  elmrsubrn  32664  mrsubco  32665  mrsubvrs  32666  mvhf  32702  msubvrs  32704  mclsax  32713  nodenselem5  33089  nosupres  33104  linerflx1  33507  linerflx2  33509  fwddifnval  33521  elhf2  33533  neibastop2lem  33605  icoreunrn  34522  relowlssretop  34526  sucneqond  34528  matunitlindflem2  34770  poimirlem4  34777  poimirlem20  34793  poimirlem30  34803  broucube  34807  opnmbllem0  34809  areacirclem2  34864  areacirclem4  34866  blssp  34912  sstotbnd2  34933  totbndbnd  34948  prdstotbnd  34953  cnpwstotbnd  34956  heiborlem9  34978  exidcl  35035  exidresid  35038  grpokerinj  35052  iscringd  35157  erim2  35791  prter3  35898  toycom  35989  islfld  36078  lshpsmreu  36125  ldualelvbase  36143  ldualssvscl  36174  lkreqN  36186  lkrlspeqN  36187  erng1lem  38003  erngdvlem4  38007  erng0g  38010  erng1r  38011  erngdvlem4-rN  38015  dva0g  38043  dia1dim2  38078  dia1dimid  38079  dia2dimlem5  38084  dvhelvbasei  38104  dvhvaddass  38113  tendoinvcl  38120  tendolinv  38121  tendorinv  38122  dvhgrp  38123  dvhlveclem  38124  cdlemn4  38214  lcfrlem12N  38570  lcfrlem15  38573  lcdvscl  38621  lcdlssvscl  38622  lcdvsass  38623  lcdvs0N  38632  mapdincl  38677  mapdin  38678  mapdlsmcl  38679  mapdcnvatN  38682  mapdpglem2  38689  mapdpglem12  38699  mapdpglem18  38705  mapdpglem21  38708  mapdpglem22  38709  mapdpglem28  38717  mapdpglem30  38718  hdmaprnlem3N  38866  hdmaprnlem3uN  38867  hdmaprnlem7N  38871  hdmaprnlem8N  38872  hdmaprnlem9N  38873  hdmaprnlem3eN  38874  hdmaprnlem16N  38878  hgmapdcl  38906  hgmapval1  38909  hgmaprnlem4N  38915  hdmapinvlem1  38934  fnsnbt  38998  selvval2lem2  39011  selvval2lem4  39014  fltnltalem  39152  wepwsolem  39520  kercvrlsm  39561  dfacbasgrp  39586  imo72b2lem0  40394  grurankcld  40446  grumnudlem  40498  grumnud  40499  inaex  40510  gruex  40511  dvconstbi  40543  cncmpmax  41166  iooabslt  41650  fmul01lt1lem2  41742  limciccioolb  41778  limcicciooub  41794  limsuppnfdlem  41858  climrescn  41905  climxrrelem  41906  climxrre  41907  liminflimsupxrre  41974  xlimmnfvlem2  41990  xlimpnfvlem2  41994  fsumcncf  42037  ioccncflimc  42044  icocncflimc  42048  cncfiooicclem1  42052  dvbdfbdioolem2  42090  dvnmul  42104  stoweidlem26  42188  stoweidlem34  42196  stoweidlem48  42210  stoweidlem59  42221  dirkercncflem3  42267  fourierdlem32  42301  fourierdlem41  42310  fourierdlem51  42319  fourierdlem63  42331  fourierdlem82  42350  fourierdlem85  42353  fourierdlem93  42361  fourierdlem111  42379  fourierdlem114  42382  etransclem35  42431  hspdifhsp  42775  opnvonmbllem1  42791  ovnovollem1  42815  mbfresmf  42893  smfaddlem1  42916  smfsuplem1  42962  smflimsuplem5  42975  fzoopth  43404  setsidel  43413  setsnidel  43414  imasetpreimafvbijlemf  43438  prelspr  43525  rnghmsubcsetclem1  44174  rngccatidALTV  44188  zrinitorngc  44199  zrtermorngc  44200  zrzeroorngc  44201  rhmsubcsetclem1  44220  rhmsubcrngclem1  44226  funcringcsetcALTV2lem3  44237  funcringcsetcALTV2lem8  44242  ringccatidALTV  44251  funcringcsetclem3ALTV  44260  funcringcsetclem8ALTV  44265  irinitoringc  44268  zrtermoringc  44269  zrninitoringc  44270  nzerooringczr  44271  srhmsubclem2  44273  srhmsubc  44275  srhmsubcALTVlem1  44291  srhmsubcALTV  44293  rhmsubcALTVlem3  44305  lcosslsp  44421  nnolog2flm1  44578
  Copyright terms: Public domain W3C validator