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

Theorem eleqtrrd 2507
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 2435 . 2  |-  ( ph  ->  B  =  C )
41, 3eleqtrd 2506 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725
This theorem is referenced by:  3eltr4d  2511  disjxiun  4196  elimdelov  6139  fnwelem  6447  tfrlem13  6637  tz7.44-2  6651  omordi  6795  oneo  6810  omeulem2  6812  oeordi  6816  oeeui  6831  nnneo  6880  erref  6911  omxpenlem  7195  unblem3  7347  dffi3  7422  ordtypelem10  7480  oismo  7493  cantnff  7613  cantnfp1lem3  7620  cantnflem1  7629  cnfcom  7641  r1ordg  7688  r1pwss  7694  rankwflemb  7703  r1elwf  7706  rankidb  7710  rankonidlem  7738  fseqenlem2  7890  dfac12lem1  8007  dfac12lem2  8008  pwsdompw  8068  ackbij2lem3  8105  ackbij2  8107  cfsmolem  8134  isfin4-3  8179  hsmexlem4  8293  ttukeylem3  8375  ttukeylem7  8379  iundom2g  8399  fpwwe2lem9  8497  canthwelem  8509  pwfseqlem4  8521  winalim2  8555  r1wunlim  8596  tskmid  8699  fzopth  11073  fzoss2  11146  fzosubel3  11162  fzoend  11170  fzofzp1  11172  fzofzp1b  11173  peano2fzor  11177  zmodfzo  11252  seqf1olem2  11346  bcn2  11593  ccatval3  11730  swrdccat2  11758  splfv1  11767  wrdeqcats1  11771  revcl  11776  revlen  11777  revccat  11781  revrev  11782  revco  11786  limsupgre  12258  summolem2a  12492  fsumm1  12520  fsumcom2  12541  prmreclem4  13270  prmreclem5  13271  vdwapid1  13326  vdwlem5  13336  vdwlem8  13339  vdwnnlem2  13347  ramub1lem1  13377  ramub1lem2  13378  mrieqvlemd  13837  mreexd  13850  mreexexlemd  13852  catcocl  13893  catass  13894  moni  13945  epii  13952  inviso1  13974  episect  13989  subccocl  14025  fullsubc  14030  funcco  14051  resf2nd  14075  funcres  14076  fthepi  14108  nati  14135  arwhoma  14183  catccatid  14240  resscatc  14243  catcisolem  14244  catcoppccl  14246  catcfuccl  14247  xpcco  14263  xpcco2  14267  xpccatid  14268  prfcl  14283  catcxpccl  14287  curf12  14307  curf1cl  14308  curf2  14309  curf2cl  14311  curfcl  14312  uncf2  14317  uncfcurf  14319  diag12  14324  diag2  14325  curf2ndf  14327  hofcl  14339  oppchofcl  14340  oyoncl  14350  yonedalem3a  14354  yonedalem4b  14356  yonedalem22  14358  yonedalem3b  14359  yonedalem3  14360  yonedainv  14361  yonffthlem  14362  acsfiindd  14586  spwpr4  14646  spwpr4c  14647  mndpropd  14704  imasmnd  14716  frmdmnd  14787  frmdgsum  14790  grpsubpropd2  14873  imasgrp  14917  subg0  14933  0ghm  15003  resghm2  15006  ghmco  15008  pwsdiagghm  15016  sylow1lem4  15218  sylow1lem5  15219  efglem  15331  efgtf  15337  efginvrel2  15342  efginvrel1  15343  efgsdmi  15347  efgs1b  15351  efgsres  15353  efgsfo  15354  efgredleme  15358  efgredlemc  15360  efgredlem  15362  efgcpbllemb  15370  frgp0  15375  frgpadd  15378  frgpinv  15379  vrgpf  15383  vrgpinv  15384  frgpuplem  15387  frgpup1  15390  frgpup2  15391  frgpup3lem  15392  frgpnabllem1  15467  frgpnabllem2  15468  gsumval3  15497  dprdfid  15558  dprdsn  15577  dprd2da  15583  dpjidcl  15599  pgpfac1lem2  15616  pgpfaclem3  15624  rngpropd  15678  imasrng  15708  divsrng2  15709  pwsco1rhm  15816  pwsco2rhm  15817  subrgunit  15869  pwsdiagrhm  15884  isabvd  15891  lmodprop2d  15989  islssd  15995  prdsvscacl  16027  prdslmodd  16028  islmhm2  16097  lmhmco  16102  lmhmplusg  16103  lmhmvsca  16104  lmhmpropd  16128  lsppreli  16145  lspsnel4  16179  lssacsex  16199  lspsnat  16200  divs1  16289  divsrhm  16291  assapropd  16369  psr0cl  16441  psrnegcl  16443  psr1cl  16449  resspsrmul  16463  subrgpsr  16465  mvrf  16471  mplmon  16509  mplcoe1  16511  subrgasclcl  16542  mplind  16545  subrgply1  16610  psrplusgpropd  16612  znf1o  16815  cssmre  16903  cldmreon  17141  neiptopreu  17180  maxlp  17194  ordttopon  17240  ordtrest2lem  17250  cnprcl2  17298  lmcnp  17351  resthauslem  17410  hauscmplem  17452  1stcfb  17491  2ndcctbss  17501  2ndcomap  17504  dis2ndc  17506  loclly  17533  hausllycmp  17540  kgeni  17552  kgenidm  17562  ptpjpre2  17595  xkoopn  17604  txopn  17617  ptpjopn  17627  ptcldmpt  17629  ptcls  17631  pthaus  17653  txkgen  17667  xkohaus  17668  xkopt  17670  txcon  17704  imastps  17736  kqid  17743  kqopn  17749  kqcld  17750  isr0  17752  indishmph  17813  pt1hmeo  17821  ptuncnv  17822  ptunhmeo  17823  t0kq  17833  filcon  17898  uzrest  17912  uffixsn  17940  fmfnfmlem2  17970  flimss2  17987  flimss1  17988  flimclslem  17999  flfcnp  18019  fclsfnflim  18042  uffclsflim  18046  fcfelbas  18051  alexsublem  18058  alexsub  18059  cnextcn  18081  cnextfres  18082  tmdgsum  18108  distgp  18112  indistgp  18113  symgtgp  18114  ghmcnp  18127  divstgpopn  18132  divstgplem  18133  divstgphaus  18135  prdstmdd  18136  prdstgpd  18137  tsmsid  18152  tsmssubm  18155  tsmsmhm  18158  tsmsadd  18159  tsmssplit  18164  utop2nei  18263  utop3cls  18264  neipcfilu  18309  cnextucn  18316  ucnextcn  18317  blpnfctr  18449  lpbl  18516  met2ndci  18535  tmsxps  18549  metcnpi  18557  metcnpi2  18558  metcnpi3  18559  metustidOLD  18572  metustid  18573  metustsymOLD  18574  metustsym  18575  metustexhalfOLD  18576  metustexhalf  18577  subgngp  18659  ngptgp  18660  sranlm  18703  nlmvscn  18706  nrginvrcn  18710  lssnlm  18719  nghmcn  18762  iccntr  18835  icccmplem2  18837  msdcn  18855  cncfmptc  18924  cncfmptid  18925  cncfmpt2f  18927  icoopnst  18947  iocopnst  18948  nmoleub2lem3  19106  nmoleub3  19110  nmhmcn  19111  ipcn  19183  cfilfcls  19210  caucfil  19219  equivcau  19236  caubl  19243  flimcfil  19249  minveclem3b  19312  minveclem4  19316  ovolicc2lem3  19398  ovolicc2lem4  19399  opnmbllem  19476  vitalilem2  19484  mbfsup  19539  mbfinf  19540  mbfi1fseqlem4  19593  limccnp  19761  limccnp2  19762  dvreslem  19779  dvres2lem  19780  dvidlem  19785  dvcnp2  19789  dvcn  19790  dvaddbr  19807  dvmulbr  19808  dvcmul  19813  dvcof  19817  dvcnvlem  19843  dvef  19847  rollelem  19856  dvlip2  19862  dvivthlem1  19875  dvivth  19877  lhop2  19882  lhop  19883  dvcnvrelem1  19884  dvcnvrelem2  19885  dvcnvre  19886  evlslem1  19919  evl1val  19931  evl1rhm  19932  pf1ind  19958  ply1rem  20069  fta1blem  20074  plycpn  20189  plyrem  20205  tayl0  20261  dvtaylp  20269  dvntaylp  20270  dvntaylp0  20271  taylthlem1  20272  taylthlem2  20273  ulmdvlem3  20301  psercn  20325  pserdv  20328  abelth  20340  efopnlem1  20530  loglesqr  20625  efrlim  20791  dchrghm  21023  dchrptlem3  21033  nbgraop  21419  nbgraf1olem5  21438  vdgr1d  21657  vdgr1b  21658  eupap1  21681  spansnid  23048  elspansn4  23058  gsumpropd2lem  24203  elzrhunit  24346  qqhcn  24358  qqhucn  24359  esumel  24425  esumsplit  24430  sigagenss2  24516  elsx  24531  sxbrsigalem0  24604  dya2icoseg  24610  probfinmeasb  24670  dstrvprob  24712  dstfrvel  24714  ballotlemrv  24760  subfacp1lem5  24853  ptpcon  24903  indispcon  24904  cvxscon  24913  cvmseu  24946  cvmliftmolem2  24952  cvmliftlem7  24961  cvmliftlem10  24964  cvmliftlem13  24966  cvmlift2lem12  24984  prodmolem2a  25244  fprodm1  25274  fprodcom2  25292  predfz  25453  linerflx1  26026  linerflx2  26028  elhf2  26059  mblfinlem  26185  areacirclem4  26225  areacirclem5  26227  locfincmp  26316  neibastop2lem  26321  blssp  26394  sstotbnd2  26415  totbndbnd  26430  prdstotbnd  26435  cnpwstotbnd  26438  heiborlem9  26460  exidcl  26483  exidresid  26486  grpokerinj  26492  iscringd  26541  prter3  26663  wepwsolem  27048  kercvrlsm  27091  dsmmlss  27120  frlmsplit2  27153  frlmup1  27160  dfacbasgrp  27183  en1uniel  27290  psgnunilem1  27326  psgnunilem5  27327  psgnunilem2  27328  psgnunilem3  27329  matbas2i  27386  matplusg2  27387  matvsca2  27388  cntzsdrg  27420  dvconstbi  27461  cncmpmax  27612  fmul01lt1lem2  27624  stoweidlem26  27684  stoweidlem34  27692  stoweidlem48  27706  stoweidlem59  27717  eldmressnsn  27895  swrdswrd  28053  swrd0swrdid  28054  swrdccatin2  28060  swrdccatin12  28068  bnj1006  29082  bnj1018  29085  bnj1121  29106  bnj1398  29155  bnj1450  29171  bnj1501  29188  toycom  29501  islfld  29591  lshpsmreu  29638  ldualelvbase  29656  ldualssvscl  29687  lkreqN  29699  lkrlspeqN  29700  erng1lem  31515  erngdvlem4  31519  erng0g  31522  erng1r  31523  erngdvlem4-rN  31527  dva0g  31556  dia1dim2  31591  dia1dimid  31592  dia2dimlem5  31597  dvhelvbasei  31617  dvhvaddass  31626  tendoinvcl  31633  tendolinv  31634  tendorinv  31635  dvhgrp  31636  dvhlveclem  31637  cdlemn4  31727  lcfrlem12N  32083  lcfrlem15  32086  lcdvscl  32134  lcdlssvscl  32135  lcdvsass  32136  lcdvs0N  32145  mapdincl  32190  mapdin  32191  mapdlsmcl  32192  mapdcnvatN  32195  mapdpglem2  32202  mapdpglem12  32212  mapdpglem18  32218  mapdpglem21  32221  mapdpglem22  32222  mapdpglem28  32230  mapdpglem30  32231  hdmaprnlem3N  32382  hdmaprnlem3uN  32383  hdmaprnlem7N  32387  hdmaprnlem8N  32388  hdmaprnlem9N  32389  hdmaprnlem3eN  32390  hdmaprnlem16N  32394  hgmapdcl  32422  hgmapval1  32425  hgmaprnlem4N  32431  hdmapinvlem1  32450
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2423  df-clel 2426
  Copyright terms: Public domain W3C validator