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

Theorem eleqtrrd 2481
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 2409 . 2  |-  ( ph  ->  B  =  C )
41, 3eleqtrd 2480 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721
This theorem is referenced by:  3eltr4d  2485  disjxiun  4169  elimdelov  6112  fnwelem  6420  tfrlem13  6610  tz7.44-2  6624  omordi  6768  oneo  6783  omeulem2  6785  oeordi  6789  oeeui  6804  nnneo  6853  erref  6884  omxpenlem  7168  unblem3  7320  dffi3  7394  ordtypelem10  7452  oismo  7465  cantnff  7585  cantnfp1lem3  7592  cantnflem1  7601  cnfcom  7613  r1ordg  7660  r1pwss  7666  rankwflemb  7675  r1elwf  7678  rankidb  7682  rankonidlem  7710  fseqenlem2  7862  dfac12lem1  7979  dfac12lem2  7980  pwsdompw  8040  ackbij2lem3  8077  ackbij2  8079  cfsmolem  8106  isfin4-3  8151  hsmexlem4  8265  ttukeylem3  8347  ttukeylem7  8351  iundom2g  8371  fpwwe2lem9  8469  canthwelem  8481  pwfseqlem4  8493  winalim2  8527  r1wunlim  8568  tskmid  8671  fzopth  11045  fzoss2  11118  fzosubel3  11134  fzoend  11142  fzofzp1  11144  fzofzp1b  11145  peano2fzor  11149  zmodfzo  11224  seqf1olem2  11318  bcn2  11565  ccatval3  11702  swrdccat2  11730  splfv1  11739  wrdeqcats1  11743  revcl  11748  revlen  11749  revccat  11753  revrev  11754  revco  11758  limsupgre  12230  summolem2a  12464  fsumm1  12492  fsumcom2  12513  prmreclem4  13242  prmreclem5  13243  vdwapid1  13298  vdwlem5  13308  vdwlem8  13311  vdwnnlem2  13319  ramub1lem1  13349  ramub1lem2  13350  mrieqvlemd  13809  mreexd  13822  mreexexlemd  13824  catcocl  13865  catass  13866  moni  13917  epii  13924  inviso1  13946  episect  13961  subccocl  13997  fullsubc  14002  funcco  14023  resf2nd  14047  funcres  14048  fthepi  14080  nati  14107  arwhoma  14155  catccatid  14212  resscatc  14215  catcisolem  14216  catcoppccl  14218  catcfuccl  14219  xpcco  14235  xpcco2  14239  xpccatid  14240  prfcl  14255  catcxpccl  14259  curf12  14279  curf1cl  14280  curf2  14281  curf2cl  14283  curfcl  14284  uncf2  14289  uncfcurf  14291  diag12  14296  diag2  14297  curf2ndf  14299  hofcl  14311  oppchofcl  14312  oyoncl  14322  yonedalem3a  14326  yonedalem4b  14328  yonedalem22  14330  yonedalem3b  14331  yonedalem3  14332  yonedainv  14333  yonffthlem  14334  acsfiindd  14558  spwpr4  14618  spwpr4c  14619  mndpropd  14676  imasmnd  14688  frmdmnd  14759  frmdgsum  14762  grpsubpropd2  14845  imasgrp  14889  subg0  14905  0ghm  14975  resghm2  14978  ghmco  14980  pwsdiagghm  14988  sylow1lem4  15190  sylow1lem5  15191  efglem  15303  efgtf  15309  efginvrel2  15314  efginvrel1  15315  efgsdmi  15319  efgs1b  15323  efgsres  15325  efgsfo  15326  efgredleme  15330  efgredlemc  15332  efgredlem  15334  efgcpbllemb  15342  frgp0  15347  frgpadd  15350  frgpinv  15351  vrgpf  15355  vrgpinv  15356  frgpuplem  15359  frgpup1  15362  frgpup2  15363  frgpup3lem  15364  frgpnabllem1  15439  frgpnabllem2  15440  gsumval3  15469  dprdfid  15530  dprdsn  15549  dprd2da  15555  dpjidcl  15571  pgpfac1lem2  15588  pgpfaclem3  15596  rngpropd  15650  imasrng  15680  divsrng2  15681  pwsco1rhm  15788  pwsco2rhm  15789  subrgunit  15841  pwsdiagrhm  15856  isabvd  15863  lmodprop2d  15961  islssd  15967  prdsvscacl  15999  prdslmodd  16000  islmhm2  16069  lmhmco  16074  lmhmplusg  16075  lmhmvsca  16076  lmhmpropd  16100  lsppreli  16117  lspsnel4  16151  lssacsex  16171  lspsnat  16172  divs1  16261  divsrhm  16263  assapropd  16341  psr0cl  16413  psrnegcl  16415  psr1cl  16421  resspsrmul  16435  subrgpsr  16437  mvrf  16443  mplmon  16481  mplcoe1  16483  subrgasclcl  16514  mplind  16517  subrgply1  16582  psrplusgpropd  16584  znf1o  16787  cssmre  16875  cldmreon  17113  neiptopreu  17152  maxlp  17165  ordttopon  17211  ordtrest2lem  17221  cnprcl2  17269  lmcnp  17322  resthauslem  17381  hauscmplem  17423  1stcfb  17461  2ndcctbss  17471  2ndcomap  17474  dis2ndc  17476  loclly  17503  hausllycmp  17510  kgeni  17522  kgenidm  17532  ptpjpre2  17565  xkoopn  17574  txopn  17587  ptpjopn  17597  ptcldmpt  17599  ptcls  17601  pthaus  17623  txkgen  17637  xkohaus  17638  xkopt  17640  txcon  17674  imastps  17706  kqid  17713  kqopn  17719  kqcld  17720  isr0  17722  indishmph  17783  pt1hmeo  17791  ptuncnv  17792  ptunhmeo  17793  t0kq  17803  filcon  17868  uzrest  17882  uffixsn  17910  fmfnfmlem2  17940  flimss2  17957  flimss1  17958  flimclslem  17969  flfcnp  17989  fclsfnflim  18012  uffclsflim  18016  fcfelbas  18021  alexsublem  18028  alexsub  18029  cnextcn  18051  cnextfres  18052  tmdgsum  18078  distgp  18082  indistgp  18083  symgtgp  18084  ghmcnp  18097  divstgpopn  18102  divstgplem  18103  divstgphaus  18105  prdstmdd  18106  prdstgpd  18107  tsmsid  18122  tsmssubm  18125  tsmsmhm  18128  tsmsadd  18129  tsmssplit  18134  utop2nei  18233  utop3cls  18234  neipcfilu  18279  cnextucn  18286  ucnextcn  18287  blpnfctr  18419  lpbl  18486  met2ndci  18505  tmsxps  18519  metcnpi  18527  metcnpi2  18528  metcnpi3  18529  metustidOLD  18542  metustid  18543  metustsymOLD  18544  metustsym  18545  metustexhalfOLD  18546  metustexhalf  18547  subgngp  18629  ngptgp  18630  sranlm  18673  nlmvscn  18676  nrginvrcn  18680  lssnlm  18689  nghmcn  18732  iccntr  18805  icccmplem2  18807  msdcn  18825  cncfmptc  18894  cncfmptid  18895  cncfmpt2f  18897  icoopnst  18917  iocopnst  18918  nmoleub2lem3  19076  nmoleub3  19080  nmhmcn  19081  ipcn  19153  cfilfcls  19180  caucfil  19189  equivcau  19206  caubl  19213  flimcfil  19219  minveclem3b  19282  minveclem4  19286  ovolicc2lem3  19368  ovolicc2lem4  19369  opnmbllem  19446  vitalilem2  19454  mbfsup  19509  mbfinf  19510  mbfi1fseqlem4  19563  limccnp  19731  limccnp2  19732  dvreslem  19749  dvres2lem  19750  dvidlem  19755  dvcnp2  19759  dvcn  19760  dvaddbr  19777  dvmulbr  19778  dvcmul  19783  dvcof  19787  dvcnvlem  19813  dvef  19817  rollelem  19826  dvlip2  19832  dvivthlem1  19845  dvivth  19847  lhop2  19852  lhop  19853  dvcnvrelem1  19854  dvcnvrelem2  19855  dvcnvre  19856  evlslem1  19889  evl1val  19901  evl1rhm  19902  pf1ind  19928  ply1rem  20039  fta1blem  20044  plycpn  20159  plyrem  20175  tayl0  20231  dvtaylp  20239  dvntaylp  20240  dvntaylp0  20241  taylthlem1  20242  taylthlem2  20243  ulmdvlem3  20271  psercn  20295  pserdv  20298  abelth  20310  efopnlem1  20500  loglesqr  20595  efrlim  20761  dchrghm  20993  dchrptlem3  21003  nbgraop  21389  nbgraf1olem5  21408  vdgr1d  21627  vdgr1b  21628  eupap1  21651  spansnid  23018  elspansn4  23028  gsumpropd2lem  24173  elzrhunit  24316  qqhcn  24328  qqhucn  24329  esumel  24395  esumsplit  24400  sigagenss2  24486  elsx  24501  sxbrsigalem0  24574  dya2icoseg  24580  probfinmeasb  24640  dstrvprob  24682  dstfrvel  24684  ballotlemrv  24730  subfacp1lem5  24823  ptpcon  24873  indispcon  24874  cvxscon  24883  cvmseu  24916  cvmliftmolem2  24922  cvmliftlem7  24931  cvmliftlem10  24934  cvmliftlem13  24936  cvmlift2lem12  24954  prodmolem2a  25213  fprodm1  25243  fprodcom2  25261  predfz  25417  linerflx1  25987  linerflx2  25989  elhf2  26020  mblfinlem  26143  areacirclem4  26183  areacirclem5  26185  locfincmp  26274  neibastop2lem  26279  blssp  26352  sstotbnd2  26373  totbndbnd  26388  prdstotbnd  26393  cnpwstotbnd  26396  heiborlem9  26418  exidcl  26441  exidresid  26444  grpokerinj  26450  iscringd  26499  prter3  26621  wepwsolem  27006  kercvrlsm  27049  dsmmlss  27078  frlmsplit2  27111  frlmup1  27118  dfacbasgrp  27141  en1uniel  27248  psgnunilem1  27284  psgnunilem5  27285  psgnunilem2  27286  psgnunilem3  27287  matbas2i  27344  matplusg2  27345  matvsca2  27346  cntzsdrg  27378  dvconstbi  27419  cncmpmax  27570  fmul01lt1lem2  27582  stoweidlem26  27642  stoweidlem34  27650  stoweidlem48  27664  stoweidlem59  27675  eldmressnsn  27853  swrdswrd  28011  swrd0swrdid  28012  swrdccatin2  28018  swrdccatin12  28026  bnj1006  29036  bnj1018  29039  bnj1121  29060  bnj1398  29109  bnj1450  29125  bnj1501  29142  toycom  29455  islfld  29545  lshpsmreu  29592  ldualelvbase  29610  ldualssvscl  29641  lkreqN  29653  lkrlspeqN  29654  erng1lem  31469  erngdvlem4  31473  erng0g  31476  erng1r  31477  erngdvlem4-rN  31481  dva0g  31510  dia1dim2  31545  dia1dimid  31546  dia2dimlem5  31551  dvhelvbasei  31571  dvhvaddass  31580  tendoinvcl  31587  tendolinv  31588  tendorinv  31589  dvhgrp  31590  dvhlveclem  31591  cdlemn4  31681  lcfrlem12N  32037  lcfrlem15  32040  lcdvscl  32088  lcdlssvscl  32089  lcdvsass  32090  lcdvs0N  32099  mapdincl  32144  mapdin  32145  mapdlsmcl  32146  mapdcnvatN  32149  mapdpglem2  32156  mapdpglem12  32166  mapdpglem18  32172  mapdpglem21  32175  mapdpglem22  32176  mapdpglem28  32184  mapdpglem30  32185  hdmaprnlem3N  32336  hdmaprnlem3uN  32337  hdmaprnlem7N  32341  hdmaprnlem8N  32342  hdmaprnlem9N  32343  hdmaprnlem3eN  32344  hdmaprnlem16N  32348  hgmapdcl  32376  hgmapval1  32379  hgmaprnlem4N  32385  hdmapinvlem1  32404
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator