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

Theorem eleqtrrd 2690
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 2615 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrd 2689 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2602  df-clel 2605
This theorem is referenced by:  3eltr4d  2702  disjxiun  4573  disjxiunOLD  4574  eldmressnsn  5346  elimdelov  6612  elovmpt3rab1  6768  fnwelem  7156  tfrlem13  7350  tz7.44-2  7367  omordi  7510  oneo  7525  omeulem2  7527  oeordi  7531  oeeui  7546  nnneo  7595  erref  7626  en1uniel  7891  omxpenlem  7923  unblem3  8076  dffi3  8197  ordtypelem10  8292  oismo  8305  cantnff  8431  cantnfp1lem3  8437  cantnflem1  8446  cnfcom  8457  r1ordg  8501  r1pwss  8507  rankwflemb  8516  r1elwf  8519  rankidb  8523  rankonidlem  8551  fseqenlem2  8708  dfac12lem1  8825  dfac12lem2  8826  pwsdompw  8886  ackbij2lem3  8923  ackbij2  8925  cfsmolem  8952  isfin4-3  8997  hsmexlem4  9111  ttukeylem3  9193  ttukeylem7  9197  iundom2g  9218  fpwwe2lem9  9316  canthwelem  9328  pwfseqlem4  9340  winalim2  9374  r1wunlim  9415  tskmid  9518  fzopth  12204  predfz  12288  fzoss2  12320  fz1fzo0m1  12338  fzo0addel  12344  fzo0addelr  12345  fzosubel3  12351  elfzomin  12361  elfzonlteqm1  12365  fzoend  12380  fzofzp1  12386  fzofzp1b  12387  peano2fzor  12396  zmodfzo  12510  seqf1olem2  12658  bcn2  12923  swrdccat2  13256  swrdswrd  13258  swrdccatin12  13288  splfv1  13303  revcl  13307  revlen  13308  revccat  13312  revrev  13313  cshwidxmod  13346  revco  13377  limsupgre  14006  summolem2a  14239  fsumm1  14270  fsumcom2  14293  fsumcom2OLD  14294  prodmolem2a  14449  fprodm1  14482  fprodcom2  14499  fprodcom2OLD  14500  prmreclem4  15407  prmreclem5  15408  vdwapid1  15463  vdwlem5  15473  vdwlem8  15476  vdwnnlem2  15484  ramub1lem1  15514  ramub1lem2  15515  mrieqvlemd  16058  mreexd  16071  mreexexlemd  16073  catcocl  16115  catass  16116  moni  16165  epii  16172  inviso1  16195  episect  16214  invisoinvl  16219  catsubcat  16268  subccocl  16274  fullsubc  16279  funcco  16300  resf2nd  16324  funcres  16325  fthepi  16357  nati  16384  arwhoma  16464  catccatid  16521  resscatc  16524  catcisolem  16525  catcoppccl  16527  catcfuccl  16528  estrreslem2  16547  funcestrcsetclem3  16551  funcestrcsetclem8  16556  funcsetcestrclem3  16565  funcsetcestrclem8  16571  xpcco  16592  xpcco2  16596  xpccatid  16597  prfcl  16612  catcxpccl  16616  curf12  16636  curf1cl  16637  curf2  16638  curf2cl  16640  curfcl  16641  uncf2  16646  uncfcurf  16648  diag12  16653  diag2  16654  curf2ndf  16656  hofcl  16668  oppchofcl  16669  oyoncl  16679  yonedalem3a  16683  yonedalem4b  16685  yonedalem22  16687  yonedalem3b  16688  yonedalem3  16689  yonedainv  16690  yonffthlem  16691  latcl2  16817  latlem  16818  latjcom  16828  latmcom  16844  clatlem  16880  clatlubcl2  16882  clatglbcl2  16884  acsfiindd  16946  gsumpropd2lem  17042  mndpropd  17085  imasmnd  17097  frmdmnd  17165  frmdgsum  17168  grpsubpropd2  17290  imasgrp  17300  subg0  17369  0ghm  17443  resghm2  17446  ghmco  17449  pwsdiagghm  17457  psgnunilem1  17682  psgnunilem5  17683  psgnunilem2  17684  psgnunilem3  17685  sylow1lem4  17785  sylow1lem5  17786  efglem  17898  efgtf  17904  efginvrel2  17909  efginvrel1  17910  efgsdmi  17914  efgs1b  17918  efgsres  17920  efgsfo  17921  efgredleme  17925  efgredlemc  17927  efgredlem  17929  efgcpbllemb  17937  frgp0  17942  frgpadd  17945  frgpinv  17946  vrgpf  17950  vrgpinv  17951  frgpuplem  17954  frgpup1  17957  frgpup2  17958  frgpup3lem  17959  frgpnabllem1  18045  frgpnabllem2  18046  gsumval3  18077  dprdfid  18185  dprdsn  18204  dprd2da  18210  dpjidcl  18226  pgpfac1lem2  18243  pgpfaclem3  18251  ringpropd  18351  imasring  18388  qusring2  18389  pwsco1rhm  18507  pwsco2rhm  18508  subrgunit  18567  pwsdiagrhm  18582  isabvd  18589  lmodprop2d  18694  islssd  18703  prdsvscacl  18735  prdslmodd  18736  islmhm2  18805  lmhmco  18810  lmhmplusg  18811  lmhmvsca  18812  lmhmpropd  18840  lsppreli  18857  lspsnel4  18891  lssacsex  18911  lspsnat  18912  qus1  19002  qusrhm  19004  assapropd  19094  psr0cl  19161  psrnegcl  19163  psr1cl  19169  resspsrmul  19184  subrgpsr  19186  mvrf  19191  mplmon  19230  mplcoe1  19232  subrgasclcl  19266  mplind  19269  evlslem1  19282  subrgply1  19370  psrplusgpropd  19373  ply1coe  19433  cply1coe0bi  19437  lply1binomsc  19444  evls1val  19452  evls1rhm  19454  evl1val  19460  evl1rhm  19463  pf1ind  19486  evl1scvarpw  19494  znf1o  19664  cssmre  19798  dsmmlss  19849  frlmsplit2  19873  frlmbas3  19876  frlmup1  19898  matbas2i  19989  matplusg2  19994  matvsca2  19995  matsubgcell  20001  matvscacell  20003  mpt2matmul  20013  mavmulval  20112  mavmulcl  20114  mavmulass  20116  mavmul0  20119  mavmumamul1  20122  m1detdiag  20164  cramerimplem2  20251  mat2pmatmul  20297  mat2pmatlin  20301  monmatcollpw  20345  pmatcollpwfi  20348  mply1topmatcl  20371  pm2mpghm  20382  pm2mpmhmlem2  20385  pm2mp  20391  chpmat1dlem  20401  chpmat1d  20402  chpdmatlem0  20403  chpscmat  20408  chpscmatgsumbin  20410  chpscmatgsummon  20411  chfacfscmulcl  20423  cpmadugsumlemB  20440  cpmadugsumlemC  20441  chcoeffeqlem  20451  cldmreon  20650  neiptopreu  20689  maxlp  20703  ordttopon  20749  ordtrest2lem  20759  cnprcl2  20807  lmcnp  20860  resthauslem  20919  hauscmplem  20961  1stcfb  21000  2ndcctbss  21010  2ndcomap  21013  dis2ndc  21015  loclly  21042  hausllycmp  21049  locfincmp  21081  dissnref  21083  kgeni  21092  kgenidm  21102  ptpjpre2  21135  xkoopn  21144  txopn  21157  ptpjopn  21167  ptcldmpt  21169  ptcls  21171  pthaus  21193  txkgen  21207  xkohaus  21208  xkopt  21210  txcon  21244  imastps  21276  kqid  21283  kqopn  21289  kqcld  21290  isr0  21292  indishmph  21353  pt1hmeo  21361  ptuncnv  21362  ptunhmeo  21363  t0kq  21373  filcon  21439  uzrest  21453  uffixsn  21481  fmfnfmlem2  21511  flimss2  21528  flimss1  21529  flimclslem  21540  flfcnp  21560  fclsfnflim  21583  uffclsflim  21587  fcfelbas  21592  alexsublem  21600  alexsub  21601  cnextcn  21623  cnextfres1  21624  tmdgsum  21651  distgp  21655  indistgp  21656  symgtgp  21657  ghmcnp  21670  qustgpopn  21675  qustgplem  21676  qustgphaus  21678  prdstmdd  21679  prdstgpd  21680  tsmsid  21695  tsmssubm  21698  tsmsmhm  21701  tsmsadd  21702  tsmssplit  21707  utop2nei  21806  utop3cls  21807  neipcfilu  21852  cnextucn  21859  ucnextcn  21860  blpnfctr  21992  lpbl  22059  met2ndci  22078  tmsxps  22092  metcnpi  22100  metcnpi2  22101  metcnpi3  22102  metustid  22110  metustsym  22111  metustexhalf  22112  subgngp  22187  ngptgp  22188  sranlm  22231  nlmvscn  22234  nrginvrcn  22239  lssnlm  22248  nghmcn  22291  iccntr  22364  icccmplem2  22366  msdcn  22384  cncfmptc  22453  cncfmptid  22454  cncfmpt2f  22456  icoopnst  22477  iocopnst  22478  nmoleub2lem3  22654  nmoleub3  22658  nmhmcn  22659  ipcn  22771  cfilfcls  22798  caucfil  22807  equivcau  22824  caubl  22831  flimcfil  22837  rrxdstprj1  22917  minveclem3b  22924  minveclem4  22928  ovolicc2lem3  23011  ovolicc2lem4  23012  opnmbllem  23092  vitalilem2  23101  mbfsup  23154  mbfinf  23155  mbfi1fseqlem4  23208  limccnp  23378  limccnp2  23379  dvreslem  23396  dvres2lem  23397  dvidlem  23402  dvcnp2  23406  dvcn  23407  dvaddbr  23424  dvmulbr  23425  dvcmul  23430  dvcof  23434  dvcnvlem  23460  dvef  23464  rollelem  23473  dvlip2  23479  dvivthlem1  23492  dvivth  23494  lhop2  23499  lhop  23500  dvcnvrelem1  23501  dvcnvrelem2  23502  dvcnvre  23503  ply1rem  23644  fta1blem  23649  plycpn  23765  plyrem  23781  tayl0  23837  dvtaylp  23845  dvntaylp  23846  dvntaylp0  23847  taylthlem1  23848  taylthlem2  23849  ulmdvlem3  23877  psercn  23901  pserdv  23904  abelth  23916  efabl  24017  efopnlem1  24119  loglesqrt  24216  relogbf  24246  efrlim  24413  dchrghm  24698  dchrptlem3  24708  tgbtwntriv2  25099  tgbtwnne  25102  ercgrg  25130  tgidinside  25184  tgbtwnconn1  25188  tglnne  25241  tglnne0  25253  tglnpt2  25254  tglineneq  25257  ncolncol  25259  coltr3  25261  mirln  25289  mirln2  25290  mirconn  25291  krippenlem  25303  footex  25331  colperpexlem3  25342  mideulem2  25344  opphllem  25345  oppne3  25353  opphllem1  25357  opphllem2  25358  opphllem4  25360  oppperpex  25363  opphl  25364  hlpasch  25366  hpgerlem  25375  colhp  25380  midbtwn  25389  lmieu  25394  lmiisolem  25406  sacgr  25440  f1otrg  25469  f1otrge  25470  ebtwntg  25580  ecgrtg  25581  eengtrkg  25583  eengtrkge  25584  nbgraop  25718  nbgraf1olem5  25740  wwlknext  26018  wwlkm1edg  26029  wwlkextproplem3  26037  clwwlkel  26087  vdgr1d  26196  vdgr1b  26197  eupap1  26269  extwwlkfablem2  26371  numclwwlkovf2ex  26379  numclwlk1lem2foa  26384  numclwwlk2lem1  26395  numclwlk2lem2f  26396  spansnid  27612  elspansn4  27622  submarchi  28877  psgnfzto1stlem  28987  1smat1  29004  submat1n  29005  lmatfval  29014  lmatcl  29016  mdetpmtr1  29023  madjusmdetlem4  29030  qtopt1  29036  qtophaus  29037  locfinref  29042  ordtrest2NEWlem  29102  elzrhunit  29157  qqhcn  29169  qqhucn  29170  esumel  29242  esumsplit  29248  sigagenss2  29346  elsx  29390  sxbrsigalem0  29466  dya2icoseg  29472  eulerpartlemb  29563  eulerpartlemgvv  29571  iwrdsplit  29582  sseqfv2  29589  probfinmeasb  29624  dstrvprob  29666  dstfrvel  29668  ballotlemrv  29714  signstfvn  29778  signstfvp  29780  signstfveq0  29786  signsvtp  29792  signsvtn  29793  bnj1006  30089  bnj1018  30092  bnj1121  30113  bnj1398  30162  bnj1450  30178  bnj1501  30195  subfacp1lem5  30226  ptpcon  30275  indispcon  30276  cvxscon  30285  cvmseu  30318  cvmliftmolem2  30324  cvmliftlem7  30333  cvmliftlem10  30336  cvmliftlem13  30338  cvmlift2lem12  30356  mrsubcv  30467  mrsubff  30469  mrsubrn  30470  mrsubccat  30475  elmrsubrn  30477  mrsubco  30478  mrsubvrs  30479  mvhf  30515  msubvrs  30517  mclsax  30526  linerflx1  31232  linerflx2  31234  fwddifnval  31246  elhf2  31258  neibastop2lem  31331  icoreunrn  32179  relowlssretop  32183  sucneqond  32185  matunitlindflem2  32372  poimirlem4  32379  poimirlem20  32395  poimirlem30  32405  broucube  32409  opnmbllem0  32411  areacirclem2  32467  areacirclem4  32469  blssp  32518  sstotbnd2  32539  totbndbnd  32554  prdstotbnd  32559  cnpwstotbnd  32562  heiborlem9  32584  exidcl  32641  exidresid  32644  grpokerinj  32658  iscringd  32763  prter3  32981  toycom  33074  islfld  33163  lshpsmreu  33210  ldualelvbase  33228  ldualssvscl  33259  lkreqN  33271  lkrlspeqN  33272  erng1lem  35089  erngdvlem4  35093  erng0g  35096  erng1r  35097  erngdvlem4-rN  35101  dva0g  35130  dia1dim2  35165  dia1dimid  35166  dia2dimlem5  35171  dvhelvbasei  35191  dvhvaddass  35200  tendoinvcl  35207  tendolinv  35208  tendorinv  35209  dvhgrp  35210  dvhlveclem  35211  cdlemn4  35301  lcfrlem12N  35657  lcfrlem15  35660  lcdvscl  35708  lcdlssvscl  35709  lcdvsass  35710  lcdvs0N  35719  mapdincl  35764  mapdin  35765  mapdlsmcl  35766  mapdcnvatN  35769  mapdpglem2  35776  mapdpglem12  35786  mapdpglem18  35792  mapdpglem21  35795  mapdpglem22  35796  mapdpglem28  35804  mapdpglem30  35805  hdmaprnlem3N  35956  hdmaprnlem3uN  35957  hdmaprnlem7N  35961  hdmaprnlem8N  35962  hdmaprnlem9N  35963  hdmaprnlem3eN  35964  hdmaprnlem16N  35968  hgmapdcl  35996  hgmapval1  35999  hgmaprnlem4N  36005  hdmapinvlem1  36024  wepwsolem  36426  kercvrlsm  36467  dfacbasgrp  36493  cntzsdrg  36587  imo72b2lem0  37283  dvconstbi  37351  cncmpmax  38010  iooabslt  38365  fmul01lt1lem2  38449  limciccioolb  38485  limcicciooub  38501  fsumcncf  38560  ioccncflimc  38568  icocncflimc  38572  cncfiooicclem1  38576  dvbdfbdioolem2  38616  dvnmul  38630  stoweidlem26  38716  stoweidlem34  38724  stoweidlem48  38738  stoweidlem59  38749  dirkercncflem3  38795  fourierdlem32  38829  fourierdlem41  38838  fourierdlem51  38847  fourierdlem63  38859  fourierdlem82  38878  fourierdlem85  38881  fourierdlem93  38889  fourierdlem111  38907  fourierdlem114  38910  etransclem35  38959  hspdifhsp  39303  opnvonmbllem1  39319  ovnovollem1  39343  mbfresmf  39423  smfaddlem1  39446  pfxccat1  40071  pfxccatin12  40086  repswpfx  40097  fzoopth  40180  upgr1eop  40335  usgredg3  40438  uspgr1eop  40468  usgr1eop  40471  subgruhgredgd  40503  vtxdun  40691  vtxdfiun  40692  1loopgruspgr  40710  1loopgredg  40711  1loopgrvd2  40713  1hevtxdg1  40716  1egrvtxdg1  40720  1egrvtxdg0  40722  umgr2v2e  40736  1wlkres  40874  1wlkp1lem4  40880  1wlkp1  40885  1wlkiswwlks1  41059  wwlksm1edg  41073  wwlksnext  41094  wwlksnextproplem1  41110  wwlksnextproplem3  41112  clwwlksel  41216  11wlkdlem2  41300  trlsegvdeg  41390  eupth2lem3lem1  41391  eupth2lem3lem2  41392  rspc2vd  41432  av-extwwlkfablem2  41505  av-extwwlkfab  41515  av-numclwlk1lem2foa  41516  av-numclwlk2lem2f  41528  rnghmsubcsetclem1  41762  rngccatidALTV  41776  zrinitorngc  41787  zrtermorngc  41788  zrzeroorngc  41789  rhmsubcsetclem1  41808  rhmsubcrngclem1  41814  funcringcsetcALTV2lem3  41825  funcringcsetcALTV2lem8  41830  ringccatidALTV  41839  funcringcsetclem3ALTV  41848  funcringcsetclem8ALTV  41853  irinitoringc  41856  zrtermoringc  41857  zrninitoringc  41858  nzerooringczr  41859  srhmsubclem2  41861  srhmsubc  41863  srhmsubcALTVlem2  41880  srhmsubcALTV  41882  rhmsubcALTVlem3  41894  lcosslsp  42016  nnolog2flm1  42177
  Copyright terms: Public domain W3C validator