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

Theorem eleqtrrd 2691
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 2616 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrd 2690 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606
This theorem is referenced by:  3eltr4d  2703  disjxiun  4579  disjxiunOLD  4580  eldmressnsn  5359  elimdelov  6634  elovmpt3rab1  6791  fnwelem  7179  tfrlem13  7373  tz7.44-2  7390  omordi  7533  oneo  7548  omeulem2  7550  oeordi  7554  oeeui  7569  nnneo  7618  erref  7649  en1uniel  7914  omxpenlem  7946  unblem3  8099  dffi3  8220  ordtypelem10  8315  oismo  8328  cantnff  8454  cantnfp1lem3  8460  cantnflem1  8469  cnfcom  8480  r1ordg  8524  r1pwss  8530  rankwflemb  8539  r1elwf  8542  rankidb  8546  rankonidlem  8574  fseqenlem2  8731  dfac12lem1  8848  dfac12lem2  8849  pwsdompw  8909  ackbij2lem3  8946  ackbij2  8948  cfsmolem  8975  isfin4-3  9020  hsmexlem4  9134  ttukeylem3  9216  ttukeylem7  9220  iundom2g  9241  fpwwe2lem9  9339  canthwelem  9351  pwfseqlem4  9363  winalim2  9397  r1wunlim  9438  tskmid  9541  fzopth  12249  predfz  12333  fzoss2  12365  fz1fzo0m1  12383  fzo0addel  12389  fzo0addelr  12390  fzosubel3  12396  elfzomin  12406  elfzonlteqm1  12410  fzoend  12425  fzofzp1  12431  fzofzp1b  12432  peano2fzor  12441  zmodfzo  12555  seqf1olem2  12703  bcn2  12968  swrdccat2  13310  swrdswrd  13312  swrdccatin12  13342  splfv1  13357  revcl  13361  revlen  13362  revccat  13366  revrev  13367  cshwidxmod  13400  revco  13431  limsupgre  14060  summolem2a  14293  fsumm1  14324  fsumcom2  14347  fsumcom2OLD  14348  prodmolem2a  14503  fprodm1  14536  fprodcom2  14553  fprodcom2OLD  14554  prmreclem4  15461  prmreclem5  15462  vdwapid1  15517  vdwlem5  15527  vdwlem8  15530  vdwnnlem2  15538  ramub1lem1  15568  ramub1lem2  15569  mrieqvlemd  16112  mreexd  16125  mreexexlemd  16127  catcocl  16169  catass  16170  moni  16219  epii  16226  inviso1  16249  episect  16268  invisoinvl  16273  catsubcat  16322  subccocl  16328  fullsubc  16333  funcco  16354  resf2nd  16378  funcres  16379  fthepi  16411  nati  16438  arwhoma  16518  catccatid  16575  resscatc  16578  catcisolem  16579  catcoppccl  16581  catcfuccl  16582  estrreslem2  16601  funcestrcsetclem3  16605  funcestrcsetclem8  16610  funcsetcestrclem3  16619  funcsetcestrclem8  16625  xpcco  16646  xpcco2  16650  xpccatid  16651  prfcl  16666  catcxpccl  16670  curf12  16690  curf1cl  16691  curf2  16692  curf2cl  16694  curfcl  16695  uncf2  16700  uncfcurf  16702  diag12  16707  diag2  16708  curf2ndf  16710  hofcl  16722  oppchofcl  16723  oyoncl  16733  yonedalem3a  16737  yonedalem4b  16739  yonedalem22  16741  yonedalem3b  16742  yonedalem3  16743  yonedainv  16744  yonffthlem  16745  latcl2  16871  latlem  16872  latjcom  16882  latmcom  16898  clatlem  16934  clatlubcl2  16936  clatglbcl2  16938  acsfiindd  17000  gsumpropd2lem  17096  mndpropd  17139  imasmnd  17151  frmdmnd  17219  frmdgsum  17222  grpsubpropd2  17344  imasgrp  17354  subg0  17423  0ghm  17497  resghm2  17500  ghmco  17503  pwsdiagghm  17511  psgnunilem1  17736  psgnunilem5  17737  psgnunilem2  17738  psgnunilem3  17739  sylow1lem4  17839  sylow1lem5  17840  efglem  17952  efgtf  17958  efginvrel2  17963  efginvrel1  17964  efgsdmi  17968  efgs1b  17972  efgsres  17974  efgsfo  17975  efgredleme  17979  efgredlemc  17981  efgredlem  17983  efgcpbllemb  17991  frgp0  17996  frgpadd  17999  frgpinv  18000  vrgpf  18004  vrgpinv  18005  frgpuplem  18008  frgpup1  18011  frgpup2  18012  frgpup3lem  18013  frgpnabllem1  18099  frgpnabllem2  18100  gsumval3  18131  dprdfid  18239  dprdsn  18258  dprd2da  18264  dpjidcl  18280  pgpfac1lem2  18297  pgpfaclem3  18305  ringpropd  18405  imasring  18442  qusring2  18443  pwsco1rhm  18561  pwsco2rhm  18562  subrgunit  18621  pwsdiagrhm  18636  isabvd  18643  lmodprop2d  18748  islssd  18757  prdsvscacl  18789  prdslmodd  18790  islmhm2  18859  lmhmco  18864  lmhmplusg  18865  lmhmvsca  18866  lmhmpropd  18894  lsppreli  18911  lspsnel4  18945  lssacsex  18965  lspsnat  18966  qus1  19056  qusrhm  19058  assapropd  19148  psr0cl  19215  psrnegcl  19217  psr1cl  19223  resspsrmul  19238  subrgpsr  19240  mvrf  19245  mplmon  19284  mplcoe1  19286  subrgasclcl  19320  mplind  19323  evlslem1  19336  subrgply1  19424  psrplusgpropd  19427  ply1coe  19487  cply1coe0bi  19491  lply1binomsc  19498  evls1val  19506  evls1rhm  19508  evl1val  19514  evl1rhm  19517  pf1ind  19540  evl1scvarpw  19548  znf1o  19719  cssmre  19856  dsmmlss  19907  frlmsplit2  19931  frlmbas3  19934  frlmup1  19956  matbas2i  20047  matplusg2  20052  matvsca2  20053  matsubgcell  20059  matvscacell  20061  mpt2matmul  20071  mavmulval  20170  mavmulcl  20172  mavmulass  20174  mavmul0  20177  mavmumamul1  20180  m1detdiag  20222  cramerimplem2  20309  mat2pmatmul  20355  mat2pmatlin  20359  monmatcollpw  20403  pmatcollpwfi  20406  mply1topmatcl  20429  pm2mpghm  20440  pm2mpmhmlem2  20443  pm2mp  20449  chpmat1dlem  20459  chpmat1d  20460  chpdmatlem0  20461  chpscmat  20466  chpscmatgsumbin  20468  chpscmatgsummon  20469  chfacfscmulcl  20481  cpmadugsumlemB  20498  cpmadugsumlemC  20499  chcoeffeqlem  20509  cldmreon  20708  neiptopreu  20747  maxlp  20761  ordttopon  20807  ordtrest2lem  20817  cnprcl2  20865  lmcnp  20918  resthauslem  20977  hauscmplem  21019  1stcfb  21058  2ndcctbss  21068  2ndcomap  21071  dis2ndc  21073  loclly  21100  hausllycmp  21107  locfincmp  21139  dissnref  21141  kgeni  21150  kgenidm  21160  ptpjpre2  21193  xkoopn  21202  txopn  21215  ptpjopn  21225  ptcldmpt  21227  ptcls  21229  pthaus  21251  txkgen  21265  xkohaus  21266  xkopt  21268  txcon  21302  imastps  21334  kqid  21341  kqopn  21347  kqcld  21348  isr0  21350  indishmph  21411  pt1hmeo  21419  ptuncnv  21420  ptunhmeo  21421  t0kq  21431  filcon  21497  uzrest  21511  uffixsn  21539  fmfnfmlem2  21569  flimss2  21586  flimss1  21587  flimclslem  21598  flfcnp  21618  fclsfnflim  21641  uffclsflim  21645  fcfelbas  21650  alexsublem  21658  alexsub  21659  cnextcn  21681  cnextfres1  21682  tmdgsum  21709  distgp  21713  indistgp  21714  symgtgp  21715  ghmcnp  21728  qustgpopn  21733  qustgplem  21734  qustgphaus  21736  prdstmdd  21737  prdstgpd  21738  tsmsid  21753  tsmssubm  21756  tsmsmhm  21759  tsmsadd  21760  tsmssplit  21765  utop2nei  21864  utop3cls  21865  neipcfilu  21910  cnextucn  21917  ucnextcn  21918  blpnfctr  22051  lpbl  22118  met2ndci  22137  tmsxps  22151  metcnpi  22159  metcnpi2  22160  metcnpi3  22161  metustid  22169  metustsym  22170  metustexhalf  22171  subgngp  22249  ngptgp  22250  sranlm  22298  nlmvscn  22301  nrginvrcn  22306  lssnlm  22315  nghmcn  22359  iccntr  22432  icccmplem2  22434  msdcn  22452  cncfmptc  22522  cncfmptid  22523  cncfmpt2f  22525  icoopnst  22546  iocopnst  22547  nmoleub2lem3  22723  nmoleub3  22727  nmhmcn  22728  ipcn  22853  cfilfcls  22880  caucfil  22889  equivcau  22906  caubl  22914  flimcfil  22920  rrxdstprj1  23000  minveclem3b  23007  minveclem4  23011  ovolicc2lem3  23094  ovolicc2lem4  23095  opnmbllem  23175  vitalilem2  23184  mbfsup  23237  mbfinf  23238  mbfi1fseqlem4  23291  limccnp  23461  limccnp2  23462  dvreslem  23479  dvres2lem  23480  dvidlem  23485  dvcnp2  23489  dvcn  23490  dvaddbr  23507  dvmulbr  23508  dvcmul  23513  dvcof  23517  dvcnvlem  23543  dvef  23547  rollelem  23556  dvlip2  23562  dvivthlem1  23575  dvivth  23577  lhop2  23582  lhop  23583  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcnvre  23586  ply1rem  23727  fta1blem  23732  plycpn  23848  plyrem  23864  tayl0  23920  dvtaylp  23928  dvntaylp  23929  dvntaylp0  23930  taylthlem1  23931  taylthlem2  23932  ulmdvlem3  23960  psercn  23984  pserdv  23987  abelth  23999  efabl  24100  efopnlem1  24202  loglesqrt  24299  relogbf  24329  efrlim  24496  dchrghm  24781  dchrptlem3  24791  tgbtwntriv2  25182  tgbtwnne  25185  ercgrg  25212  tgidinside  25266  tgbtwnconn1  25270  tglnne  25323  tglnne0  25335  tglnpt2  25336  tglineneq  25339  ncolncol  25341  coltr3  25343  mirln  25371  mirln2  25372  mirconn  25373  krippenlem  25385  footex  25413  colperpexlem3  25424  mideulem2  25426  opphllem  25427  oppne3  25435  opphllem1  25439  opphllem2  25440  opphllem4  25442  oppperpex  25445  opphl  25446  hlpasch  25448  hpgerlem  25457  colhp  25462  midbtwn  25471  lmieu  25476  lmiisolem  25488  sacgr  25522  f1otrg  25551  f1otrge  25552  ebtwntg  25662  ecgrtg  25663  eengtrkg  25665  eengtrkge  25666  upgr1eop  25781  nbgraop  25952  nbgraf1olem5  25974  wwlknext  26252  wwlkm1edg  26263  wwlkextproplem3  26271  clwwlkel  26321  vdgr1d  26430  vdgr1b  26431  eupap1  26503  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwlk1lem2foa  26618  numclwwlk2lem1  26629  numclwlk2lem2f  26630  spansnid  27806  elspansn4  27816  submarchi  29071  psgnfzto1stlem  29181  1smat1  29198  submat1n  29199  lmatfval  29208  lmatcl  29210  mdetpmtr1  29217  madjusmdetlem4  29224  qtopt1  29230  qtophaus  29231  locfinref  29236  ordtrest2NEWlem  29296  elzrhunit  29351  qqhcn  29363  qqhucn  29364  esumel  29436  esumsplit  29442  sigagenss2  29540  elsx  29584  sxbrsigalem0  29660  dya2icoseg  29666  eulerpartlemb  29757  eulerpartlemgvv  29765  iwrdsplit  29776  sseqfv2  29783  probfinmeasb  29818  dstrvprob  29860  dstfrvel  29862  ballotlemrv  29908  signstfvn  29972  signstfvp  29974  signstfveq0  29980  signsvtp  29986  signsvtn  29987  bnj1006  30283  bnj1018  30286  bnj1121  30307  bnj1398  30356  bnj1450  30372  bnj1501  30389  subfacp1lem5  30420  ptpcon  30469  indispcon  30470  cvxscon  30479  cvmseu  30512  cvmliftmolem2  30518  cvmliftlem7  30527  cvmliftlem10  30530  cvmliftlem13  30532  cvmlift2lem12  30550  mrsubcv  30661  mrsubff  30663  mrsubrn  30664  mrsubccat  30669  elmrsubrn  30671  mrsubco  30672  mrsubvrs  30673  mvhf  30709  msubvrs  30711  mclsax  30720  linerflx1  31426  linerflx2  31428  fwddifnval  31440  elhf2  31452  neibastop2lem  31525  icoreunrn  32383  relowlssretop  32387  sucneqond  32389  matunitlindflem2  32576  poimirlem4  32583  poimirlem20  32599  poimirlem30  32609  broucube  32613  opnmbllem0  32615  areacirclem2  32671  areacirclem4  32673  blssp  32722  sstotbnd2  32743  totbndbnd  32758  prdstotbnd  32763  cnpwstotbnd  32766  heiborlem9  32788  exidcl  32845  exidresid  32848  grpokerinj  32862  iscringd  32967  prter3  33185  toycom  33278  islfld  33367  lshpsmreu  33414  ldualelvbase  33432  ldualssvscl  33463  lkreqN  33475  lkrlspeqN  33476  erng1lem  35293  erngdvlem4  35297  erng0g  35300  erng1r  35301  erngdvlem4-rN  35305  dva0g  35334  dia1dim2  35369  dia1dimid  35370  dia2dimlem5  35375  dvhelvbasei  35395  dvhvaddass  35404  tendoinvcl  35411  tendolinv  35412  tendorinv  35413  dvhgrp  35414  dvhlveclem  35415  cdlemn4  35505  lcfrlem12N  35861  lcfrlem15  35864  lcdvscl  35912  lcdlssvscl  35913  lcdvsass  35914  lcdvs0N  35923  mapdincl  35968  mapdin  35969  mapdlsmcl  35970  mapdcnvatN  35973  mapdpglem2  35980  mapdpglem12  35990  mapdpglem18  35996  mapdpglem21  35999  mapdpglem22  36000  mapdpglem28  36008  mapdpglem30  36009  hdmaprnlem3N  36160  hdmaprnlem3uN  36161  hdmaprnlem7N  36165  hdmaprnlem8N  36166  hdmaprnlem9N  36167  hdmaprnlem3eN  36168  hdmaprnlem16N  36172  hgmapdcl  36200  hgmapval1  36203  hgmaprnlem4N  36209  hdmapinvlem1  36228  wepwsolem  36630  kercvrlsm  36671  dfacbasgrp  36697  cntzsdrg  36791  imo72b2lem0  37487  dvconstbi  37555  cncmpmax  38214  iooabslt  38568  fmul01lt1lem2  38652  limciccioolb  38688  limcicciooub  38704  fsumcncf  38763  ioccncflimc  38771  icocncflimc  38775  cncfiooicclem1  38779  dvbdfbdioolem2  38819  dvnmul  38833  stoweidlem26  38919  stoweidlem34  38927  stoweidlem48  38941  stoweidlem59  38952  dirkercncflem3  38998  fourierdlem32  39032  fourierdlem41  39041  fourierdlem51  39050  fourierdlem63  39062  fourierdlem82  39081  fourierdlem85  39084  fourierdlem93  39092  fourierdlem111  39110  fourierdlem114  39113  etransclem35  39162  hspdifhsp  39506  opnvonmbllem1  39522  ovnovollem1  39546  mbfresmf  39626  smfaddlem1  39649  pfxccat1  40273  pfxccatin12  40288  repswpfx  40299  fzoopth  40360  usgredg3  40443  uspgr1eop  40473  usgr1eop  40476  subgruhgredgd  40508  vtxdun  40696  vtxdfiun  40697  1loopgruspgr  40715  1loopgredg  40716  1loopgrvd2  40718  1hevtxdg1  40721  1egrvtxdg1  40725  1egrvtxdg0  40727  umgr2v2e  40741  1wlkres  40879  1wlkp1lem4  40885  1wlkp1  40890  1wlkiswwlks1  41064  wwlksm1edg  41078  wwlksnext  41099  wwlksnextproplem1  41115  wwlksnextproplem3  41117  clwwlksel  41221  11wlkdlem2  41305  trlsegvdeg  41395  eupth2lem3lem1  41396  eupth2lem3lem2  41397  rspc2vd  41437  av-extwwlkfablem2  41510  av-extwwlkfab  41520  av-numclwlk1lem2foa  41521  av-numclwlk2lem2f  41533  rnghmsubcsetclem1  41767  rngccatidALTV  41781  zrinitorngc  41792  zrtermorngc  41793  zrzeroorngc  41794  rhmsubcsetclem1  41813  rhmsubcrngclem1  41819  funcringcsetcALTV2lem3  41830  funcringcsetcALTV2lem8  41835  ringccatidALTV  41844  funcringcsetclem3ALTV  41853  funcringcsetclem8ALTV  41858  irinitoringc  41861  zrtermoringc  41862  zrninitoringc  41863  nzerooringczr  41864  srhmsubclem2  41866  srhmsubc  41868  srhmsubcALTVlem2  41885  srhmsubcALTV  41887  rhmsubcALTVlem3  41899  lcosslsp  42021  nnolog2flm1  42182
  Copyright terms: Public domain W3C validator