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

Theorem eleqtrrd 2515
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eleqtrrd.1  |-  ( ph  ->  A  e.  B )
eleqtrrd.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
eleqtrrd  |-  ( ph  ->  A  e.  C )

Proof of Theorem eleqtrrd
StepHypRef Expression
1 eleqtrrd.1 . 2  |-  ( ph  ->  A  e.  B )
2 eleqtrrd.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2443 . 2  |-  ( ph  ->  B  =  C )
41, 3eleqtrd 2514 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726
This theorem is referenced by:  3eltr4d  2519  disjxiun  4212  elimdelov  6156  fnwelem  6464  tfrlem13  6654  tz7.44-2  6668  omordi  6812  oneo  6827  omeulem2  6829  oeordi  6833  oeeui  6848  nnneo  6897  erref  6928  omxpenlem  7212  unblem3  7364  dffi3  7439  ordtypelem10  7499  oismo  7512  cantnff  7632  cantnfp1lem3  7639  cantnflem1  7648  cnfcom  7660  r1ordg  7707  r1pwss  7713  rankwflemb  7722  r1elwf  7725  rankidb  7729  rankonidlem  7757  fseqenlem2  7911  dfac12lem1  8028  dfac12lem2  8029  pwsdompw  8089  ackbij2lem3  8126  ackbij2  8128  cfsmolem  8155  isfin4-3  8200  hsmexlem4  8314  ttukeylem3  8396  ttukeylem7  8400  iundom2g  8420  fpwwe2lem9  8518  canthwelem  8530  pwfseqlem4  8542  winalim2  8576  r1wunlim  8617  tskmid  8720  fzopth  11094  fzoss2  11168  fzosubel3  11184  fzoend  11192  fzofzp1  11194  fzofzp1b  11195  peano2fzor  11199  zmodfzo  11274  seqf1olem2  11368  bcn2  11615  ccatval3  11752  swrdccat2  11780  splfv1  11789  wrdeqcats1  11793  revcl  11798  revlen  11799  revccat  11803  revrev  11804  revco  11808  limsupgre  12280  summolem2a  12514  fsumm1  12542  fsumcom2  12563  prmreclem4  13292  prmreclem5  13293  vdwapid1  13348  vdwlem5  13358  vdwlem8  13361  vdwnnlem2  13369  ramub1lem1  13399  ramub1lem2  13400  mrieqvlemd  13859  mreexd  13872  mreexexlemd  13874  catcocl  13915  catass  13916  moni  13967  epii  13974  inviso1  13996  episect  14011  subccocl  14047  fullsubc  14052  funcco  14073  resf2nd  14097  funcres  14098  fthepi  14130  nati  14157  arwhoma  14205  catccatid  14262  resscatc  14265  catcisolem  14266  catcoppccl  14268  catcfuccl  14269  xpcco  14285  xpcco2  14289  xpccatid  14290  prfcl  14305  catcxpccl  14309  curf12  14329  curf1cl  14330  curf2  14331  curf2cl  14333  curfcl  14334  uncf2  14339  uncfcurf  14341  diag12  14346  diag2  14347  curf2ndf  14349  hofcl  14361  oppchofcl  14362  oyoncl  14372  yonedalem3a  14376  yonedalem4b  14378  yonedalem22  14380  yonedalem3b  14381  yonedalem3  14382  yonedainv  14383  yonffthlem  14384  acsfiindd  14608  spwpr4  14668  spwpr4c  14669  mndpropd  14726  imasmnd  14738  frmdmnd  14809  frmdgsum  14812  grpsubpropd2  14895  imasgrp  14939  subg0  14955  0ghm  15025  resghm2  15028  ghmco  15030  pwsdiagghm  15038  sylow1lem4  15240  sylow1lem5  15241  efglem  15353  efgtf  15359  efginvrel2  15364  efginvrel1  15365  efgsdmi  15369  efgs1b  15373  efgsres  15375  efgsfo  15376  efgredleme  15380  efgredlemc  15382  efgredlem  15384  efgcpbllemb  15392  frgp0  15397  frgpadd  15400  frgpinv  15401  vrgpf  15405  vrgpinv  15406  frgpuplem  15409  frgpup1  15412  frgpup2  15413  frgpup3lem  15414  frgpnabllem1  15489  frgpnabllem2  15490  gsumval3  15519  dprdfid  15580  dprdsn  15599  dprd2da  15605  dpjidcl  15621  pgpfac1lem2  15638  pgpfaclem3  15646  rngpropd  15700  imasrng  15730  divsrng2  15731  pwsco1rhm  15838  pwsco2rhm  15839  subrgunit  15891  pwsdiagrhm  15906  isabvd  15913  lmodprop2d  16011  islssd  16017  prdsvscacl  16049  prdslmodd  16050  islmhm2  16119  lmhmco  16124  lmhmplusg  16125  lmhmvsca  16126  lmhmpropd  16150  lsppreli  16167  lspsnel4  16201  lssacsex  16221  lspsnat  16222  divs1  16311  divsrhm  16313  assapropd  16391  psr0cl  16463  psrnegcl  16465  psr1cl  16471  resspsrmul  16485  subrgpsr  16487  mvrf  16493  mplmon  16531  mplcoe1  16533  subrgasclcl  16564  mplind  16567  subrgply1  16632  psrplusgpropd  16634  znf1o  16837  cssmre  16925  cldmreon  17163  neiptopreu  17202  maxlp  17216  ordttopon  17262  ordtrest2lem  17272  cnprcl2  17320  lmcnp  17373  resthauslem  17432  hauscmplem  17474  1stcfb  17513  2ndcctbss  17523  2ndcomap  17526  dis2ndc  17528  loclly  17555  hausllycmp  17562  kgeni  17574  kgenidm  17584  ptpjpre2  17617  xkoopn  17626  txopn  17639  ptpjopn  17649  ptcldmpt  17651  ptcls  17653  pthaus  17675  txkgen  17689  xkohaus  17690  xkopt  17692  txcon  17726  imastps  17758  kqid  17765  kqopn  17771  kqcld  17772  isr0  17774  indishmph  17835  pt1hmeo  17843  ptuncnv  17844  ptunhmeo  17845  t0kq  17855  filcon  17920  uzrest  17934  uffixsn  17962  fmfnfmlem2  17992  flimss2  18009  flimss1  18010  flimclslem  18021  flfcnp  18041  fclsfnflim  18064  uffclsflim  18068  fcfelbas  18073  alexsublem  18080  alexsub  18081  cnextcn  18103  cnextfres  18104  tmdgsum  18130  distgp  18134  indistgp  18135  symgtgp  18136  ghmcnp  18149  divstgpopn  18154  divstgplem  18155  divstgphaus  18157  prdstmdd  18158  prdstgpd  18159  tsmsid  18174  tsmssubm  18177  tsmsmhm  18180  tsmsadd  18181  tsmssplit  18186  utop2nei  18285  utop3cls  18286  neipcfilu  18331  cnextucn  18338  ucnextcn  18339  blpnfctr  18471  lpbl  18538  met2ndci  18557  tmsxps  18571  metcnpi  18579  metcnpi2  18580  metcnpi3  18581  metustidOLD  18594  metustid  18595  metustsymOLD  18596  metustsym  18597  metustexhalfOLD  18598  metustexhalf  18599  subgngp  18681  ngptgp  18682  sranlm  18725  nlmvscn  18728  nrginvrcn  18732  lssnlm  18741  nghmcn  18784  iccntr  18857  icccmplem2  18859  msdcn  18877  cncfmptc  18946  cncfmptid  18947  cncfmpt2f  18949  icoopnst  18969  iocopnst  18970  nmoleub2lem3  19128  nmoleub3  19132  nmhmcn  19133  ipcn  19205  cfilfcls  19232  caucfil  19241  equivcau  19258  caubl  19265  flimcfil  19271  minveclem3b  19334  minveclem4  19338  ovolicc2lem3  19420  ovolicc2lem4  19421  opnmbllem  19498  vitalilem2  19506  mbfsup  19559  mbfinf  19560  mbfi1fseqlem4  19613  limccnp  19783  limccnp2  19784  dvreslem  19801  dvres2lem  19802  dvidlem  19807  dvcnp2  19811  dvcn  19812  dvaddbr  19829  dvmulbr  19830  dvcmul  19835  dvcof  19839  dvcnvlem  19865  dvef  19869  rollelem  19878  dvlip2  19884  dvivthlem1  19897  dvivth  19899  lhop2  19904  lhop  19905  dvcnvrelem1  19906  dvcnvrelem2  19907  dvcnvre  19908  evlslem1  19941  evl1val  19953  evl1rhm  19954  pf1ind  19980  ply1rem  20091  fta1blem  20096  plycpn  20211  plyrem  20227  tayl0  20283  dvtaylp  20291  dvntaylp  20292  dvntaylp0  20293  taylthlem1  20294  taylthlem2  20295  ulmdvlem3  20323  psercn  20347  pserdv  20350  abelth  20362  efopnlem1  20552  loglesqr  20647  efrlim  20813  dchrghm  21045  dchrptlem3  21055  nbgraop  21441  nbgraf1olem5  21460  vdgr1d  21679  vdgr1b  21680  eupap1  21703  spansnid  23070  elspansn4  23080  gsumpropd2lem  24225  elzrhunit  24368  qqhcn  24380  qqhucn  24381  esumel  24447  esumsplit  24452  sigagenss2  24538  elsx  24553  sxbrsigalem0  24626  dya2icoseg  24632  probfinmeasb  24692  dstrvprob  24734  dstfrvel  24736  ballotlemrv  24782  subfacp1lem5  24875  ptpcon  24925  indispcon  24926  cvxscon  24935  cvmseu  24968  cvmliftmolem2  24974  cvmliftlem7  24983  cvmliftlem10  24986  cvmliftlem13  24988  cvmlift2lem12  25006  prodmolem2a  25265  fprodm1  25295  fprodcom2  25313  predfz  25483  linerflx1  26088  linerflx2  26090  elhf2  26121  opnmbllem0  26254  areacirclem2  26307  areacirclem4  26309  locfincmp  26398  neibastop2lem  26403  blssp  26476  sstotbnd2  26497  totbndbnd  26512  prdstotbnd  26517  cnpwstotbnd  26520  heiborlem9  26542  exidcl  26565  exidresid  26568  grpokerinj  26574  iscringd  26623  prter3  26745  wepwsolem  27130  kercvrlsm  27172  dsmmlss  27201  frlmsplit2  27234  frlmup1  27241  dfacbasgrp  27264  en1uniel  27371  psgnunilem1  27407  psgnunilem5  27408  psgnunilem2  27409  psgnunilem3  27410  matbas2i  27467  matplusg2  27468  matvsca2  27469  cntzsdrg  27501  dvconstbi  27542  cncmpmax  27693  fmul01lt1lem2  27705  stoweidlem26  27765  stoweidlem34  27773  stoweidlem48  27787  stoweidlem59  27798  eldmressnsn  27976  fzoopth  28162  swrdswrd  28233  swrd0swrdid  28234  swrdccatin12  28248  cshwidx  28276  2cshw2lem1  28286  bnj1006  29404  bnj1018  29407  bnj1121  29428  bnj1398  29477  bnj1450  29493  bnj1501  29510  toycom  29844  islfld  29934  lshpsmreu  29981  ldualelvbase  29999  ldualssvscl  30030  lkreqN  30042  lkrlspeqN  30043  erng1lem  31858  erngdvlem4  31862  erng0g  31865  erng1r  31866  erngdvlem4-rN  31870  dva0g  31899  dia1dim2  31934  dia1dimid  31935  dia2dimlem5  31940  dvhelvbasei  31960  dvhvaddass  31969  tendoinvcl  31976  tendolinv  31977  tendorinv  31978  dvhgrp  31979  dvhlveclem  31980  cdlemn4  32070  lcfrlem12N  32426  lcfrlem15  32429  lcdvscl  32477  lcdlssvscl  32478  lcdvsass  32479  lcdvs0N  32488  mapdincl  32533  mapdin  32534  mapdlsmcl  32535  mapdcnvatN  32538  mapdpglem2  32545  mapdpglem12  32555  mapdpglem18  32561  mapdpglem21  32564  mapdpglem22  32565  mapdpglem28  32573  mapdpglem30  32574  hdmaprnlem3N  32725  hdmaprnlem3uN  32726  hdmaprnlem7N  32730  hdmaprnlem8N  32731  hdmaprnlem9N  32732  hdmaprnlem3eN  32733  hdmaprnlem16N  32737  hgmapdcl  32765  hgmapval1  32768  hgmaprnlem4N  32774  hdmapinvlem1  32793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-clel 2434
  Copyright terms: Public domain W3C validator