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

Theorem eleqtrrd 2360
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 2288 . 2  |-  ( ph  ->  B  =  C )
41, 3eleqtrd 2359 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  3eltr4d  2364  disjxiun  4020  elimdelov  5927  fnwelem  6230  tfrlem13  6406  tz7.44-2  6420  omordi  6564  oneo  6579  omeulem2  6581  oeordi  6585  oeeui  6600  nnneo  6649  erref  6680  omxpenlem  6963  unblem3  7111  dffi3  7184  ordtypelem10  7242  oismo  7255  cantnflt  7373  cantnff  7375  cantnfp1lem3  7382  cantnflem1  7391  cnfcom  7403  r1ordg  7450  r1pwss  7456  rankwflemb  7465  r1elwf  7468  rankidb  7472  rankonidlem  7500  fseqenlem2  7652  dfac12lem1  7769  dfac12lem2  7770  pwsdompw  7830  ackbij2lem3  7867  ackbij2  7869  cfsmolem  7896  isfin4-3  7941  hsmexlem4  8055  ttukeylem3  8138  ttukeylem7  8142  iundom2g  8162  fpwwe2lem9  8260  canthwelem  8272  pwfseqlem4  8284  winalim2  8318  r1wunlim  8359  tskmid  8462  iccf1o  10778  fzopth  10828  fzoss2  10897  fzosubel3  10910  fzoend  10914  fzofzp1  10916  fzofzp1b  10917  peano2fzor  10919  zmodfzo  10992  seqf1olem2  11086  bcn2  11331  ccatval3  11433  swrdccat2  11461  splfv1  11470  wrdeqcats1  11474  revcl  11479  revlen  11480  revccat  11484  revrev  11485  revco  11489  limsupgre  11955  summolem2a  12188  fsumm1  12216  fsumcom2  12237  prmreclem4  12966  prmreclem5  12967  vdwapid1  13022  vdwlem5  13032  vdwlem8  13035  vdwnnlem2  13043  ramub1lem1  13073  ramub1lem2  13074  mrieqvlemd  13531  mreexd  13544  mreexexlemd  13546  catcocl  13587  catass  13588  moni  13639  epii  13646  inviso1  13668  episect  13683  subccocl  13719  fullsubc  13724  funcco  13745  cofucl  13762  resf2nd  13769  funcres  13770  fthepi  13802  nati  13829  arwhoma  13877  catccatid  13934  resscatc  13937  catcisolem  13938  catcoppccl  13940  catcfuccl  13941  xpcco  13957  xpcco2  13961  xpccatid  13962  prfcl  13977  catcxpccl  13981  curf12  14001  curf1cl  14002  curf2  14003  curf2cl  14005  curfcl  14006  uncf2  14011  uncfcurf  14013  diag12  14018  diag2  14019  curf2ndf  14021  hofcl  14033  oppchofcl  14034  oyoncl  14044  yonedalem3a  14048  yonedalem4b  14050  yonedalem22  14052  yonedalem3b  14053  yonedalem3  14054  yonedainv  14055  yonffthlem  14056  acsfiindd  14280  spwpr4  14340  spwpr4c  14341  mndpropd  14398  issubmnd  14401  imasmnd  14410  pwspjmhm  14444  gsumccat  14464  frmdmnd  14481  frmdgsum  14484  grpsubpropd2  14567  imasgrp  14611  subg0  14627  subgcl  14631  0ghm  14697  resghm2  14700  ghmco  14702  pwsdiagghm  14710  sylow1lem4  14912  sylow1lem5  14913  efglem  15025  efgtf  15031  efginvrel2  15036  efginvrel1  15037  efgsdmi  15041  efgs1b  15045  efgsres  15047  efgsfo  15048  efgredleme  15052  efgredlemc  15054  efgredlem  15056  efgcpbllemb  15064  frgp0  15069  frgpadd  15072  frgpinv  15073  vrgpf  15077  vrgpinv  15078  frgpuplem  15081  frgpup1  15084  frgpup2  15085  frgpup3lem  15086  frgpnabllem1  15161  frgpnabllem2  15162  gsumval3  15191  gsumzsubmcl  15200  dprdfid  15252  dprdsn  15271  dprd2da  15277  dpjidcl  15293  dpjghm  15298  pgpfac1lem2  15310  pgpfaclem3  15318  rngpropd  15372  imasrng  15402  divsrng2  15403  pwsco1rhm  15510  pwsco2rhm  15511  subrgmcl  15557  subrgunit  15563  issubdrg  15570  pwsdiagrhm  15578  isabvd  15585  lmodprop2d  15687  islssd  15693  prdsvscacl  15725  prdslmodd  15726  islmhm2  15795  lmhmco  15800  lmhmplusg  15801  lmhmvsca  15802  lmhmpropd  15826  lsppreli  15843  lspsnel4  15877  lssacsex  15897  lspsnat  15898  divs1  15987  divsrhm  15989  assapropd  16067  psrmulcllem  16132  psrvscacl  16138  psr0cl  16139  psrnegcl  16141  psr1cl  16147  resspsrmul  16161  subrgpsr  16163  mvrf  16169  mplmon  16207  mplcoe1  16209  subrgasclcl  16240  mplind  16243  subrgply1  16311  psrplusgpropd  16313  znf1o  16505  cssmre  16593  cldmreon  16831  maxlp  16878  ordttopon  16923  ordtrest2lem  16933  cnprcl2  16981  lmcnp  17032  resthauslem  17091  imacmp  17124  hauscmplem  17133  1stcfb  17171  2ndcctbss  17181  2ndcomap  17184  dis2ndc  17186  loclly  17213  hausllycmp  17220  kgeni  17232  kgenidm  17242  ptpjpre2  17275  xkoopn  17284  txopn  17297  ptpjopn  17306  ptcldmpt  17308  ptcls  17310  pthaus  17332  txkgen  17346  xkohaus  17347  xkopt  17349  txcon  17383  imastps  17412  kqid  17419  kqopn  17425  kqcld  17426  isr0  17428  indishmph  17489  pt1hmeo  17497  ptuncnv  17498  ptunhmeo  17499  t0kq  17509  filcon  17578  uzrest  17592  uffixsn  17620  fmfnfmlem2  17650  flimss2  17667  flimss1  17668  flimclslem  17679  flfcnp  17699  fclsfnflim  17722  uffclsflim  17726  fcfelbas  17731  alexsublem  17738  alexsub  17739  tmdgsum  17778  distgp  17782  indistgp  17783  symgtgp  17784  ghmcnp  17797  divstgpopn  17802  divstgplem  17803  divstgphaus  17805  prdstmdd  17806  prdstgpd  17807  tsmsid  17822  tsmssubm  17825  tsmsmhm  17828  tsmsadd  17829  tsmssplit  17834  blpnfctr  17982  lpbl  18049  met2ndci  18068  prdsxmslem2  18075  tmsxps  18082  metcnpi  18090  metcnpi2  18091  metcnpi3  18092  subgngp  18151  ngptgp  18152  sranlm  18195  nlmvscn  18198  nrginvrcn  18202  lssnlm  18211  nghmcn  18254  iccntr  18326  icccmplem2  18328  msdcn  18346  cncfmptc  18415  cncfmptid  18416  cncfmpt2f  18418  cnmpt2pc  18426  icoopnst  18437  iocopnst  18438  nmoleub2lem3  18596  nmoleub3  18600  nmhmcn  18601  ipcn  18673  cfilfcls  18700  caucfil  18709  equivcau  18726  caubl  18733  caublcls  18734  flimcfil  18739  minveclem3b  18792  minveclem4  18796  ovolicc2lem3  18878  ovolicc2lem4  18879  opnmbllem  18956  vitalilem2  18964  mbfsup  19019  mbfinf  19020  mbfi1fseqlem4  19073  limccnp  19241  limccnp2  19242  dvreslem  19259  dvres2lem  19260  dvidlem  19265  dvcnp2  19269  dvcn  19270  dvaddbr  19287  dvmulbr  19288  dvcmul  19293  dvcof  19297  dvcnvlem  19323  dvef  19327  rollelem  19336  dvlip2  19342  dvivthlem1  19355  dvivth  19357  lhop2  19362  lhop  19363  dvcnvrelem1  19364  dvcnvrelem2  19365  dvcnvre  19366  evlslem1  19399  evl1val  19411  evl1rhm  19412  pf1ind  19438  ply1rem  19549  fta1blem  19554  plycpn  19669  plyrem  19685  tayl0  19741  dvtaylp  19749  dvntaylp  19750  dvntaylp0  19751  taylthlem1  19752  taylthlem2  19753  ulmdvlem3  19779  psercn  19802  pserdv  19805  abelth  19817  efopnlem1  20003  loglesqr  20098  efrlim  20264  dchrghm  20495  dchrptlem3  20505  spansnid  22142  elspansn4  22152  ballotlemrv  23078  gsumpropd2lem  23379  esumel  23426  esumsplit  23431  elsx  23525  dya2iocseg  23579  dstfrvel  23674  subfacp1lem5  23715  ptpcon  23764  indispcon  23765  cvxscon  23774  cvmseu  23807  cvmliftmolem2  23813  cvmliftlem7  23822  cvmliftlem10  23825  cvmliftlem13  23827  cvmlift2lem12  23845  vdgr1d  23894  vdgr1b  23895  eupap1  23900  predfz  24203  linerflx1  24772  linerflx2  24774  elhf2  24805  areacirclem4  24927  areacirclem5  24929  npincppr  25159  clfsebsr  25349  mapdiscn  25527  mapudiscn  25528  rcmob  25749  rocatval  25959  empklst  26009  lineval2a  26085  sgplpte21d1  26139  locfincmp  26304  neibastop2lem  26309  blssp  26470  sstotbnd2  26498  totbndbnd  26513  prdstotbnd  26518  cnpwstotbnd  26521  heiborlem9  26543  exidcl  26566  exidresid  26569  grpokerinj  26575  iscringd  26624  prter3  26750  wepwsolem  27138  kelac1  27161  kercvrlsm  27181  dsmmlss  27210  frlmsplit2  27243  frlmup1  27250  dfacbasgrp  27273  en1uniel  27380  psgnunilem1  27416  psgnunilem5  27417  psgnunilem2  27418  psgnunilem3  27419  matbas2i  27476  matplusg2  27477  matvsca2  27478  cntzsdrg  27510  dvconstbi  27551  fnchoice  27700  cncmpmax  27703  climsuse  27734  stoweidlem26  27775  stoweidlem34  27783  stoweidlem59  27808  eldmressnsn  27984  nbgraop  28140  bnj1006  28991  bnj1018  28994  bnj1121  29015  bnj1398  29064  bnj1450  29080  bnj1501  29097  toycom  29162  islfld  29252  lshpsmreu  29299  ldualelvbase  29317  ldualssvscl  29348  lkreqN  29360  lkrlspeqN  29361  erng1lem  31176  erngdvlem4  31180  erng0g  31183  erng1r  31184  erngdvlem4-rN  31188  dva0g  31217  dia1dim2  31252  dia1dimid  31253  dia2dimlem5  31258  dvhelvbasei  31278  dvhvaddass  31287  tendoinvcl  31294  tendolinv  31295  tendorinv  31296  dvhgrp  31297  dvhlveclem  31298  diblss  31360  cdlemn4  31388  lcfrlem12N  31744  lcfrlem15  31747  lcdvscl  31795  lcdlssvscl  31796  lcdvsass  31797  lcdvs0N  31806  mapdincl  31851  mapdin  31852  mapdlsmcl  31853  mapdcnvatN  31856  mapdpglem2  31863  mapdpglem12  31873  mapdpglem18  31879  mapdpglem21  31882  mapdpglem22  31883  mapdpglem28  31891  mapdpglem30  31892  hdmaprnlem3N  32043  hdmaprnlem3uN  32044  hdmaprnlem7N  32048  hdmaprnlem8N  32049  hdmaprnlem9N  32050  hdmaprnlem3eN  32051  hdmaprnlem16N  32055  hgmapdcl  32083  hgmapval1  32086  hgmaprnlem4N  32092  hdmapinvlem1  32111
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator