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

Theorem eleqtrrd 2373
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 2301 . 2  |-  ( ph  ->  B  =  C )
41, 3eleqtrd 2372 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696
This theorem is referenced by:  3eltr4d  2377  disjxiun  4036  elimdelov  5943  fnwelem  6246  tfrlem13  6422  tz7.44-2  6436  omordi  6580  oneo  6595  omeulem2  6597  oeordi  6601  oeeui  6616  nnneo  6665  erref  6696  omxpenlem  6979  unblem3  7127  dffi3  7200  ordtypelem10  7258  oismo  7271  cantnflt  7389  cantnff  7391  cantnfp1lem3  7398  cantnflem1  7407  cnfcom  7419  r1ordg  7466  r1pwss  7472  rankwflemb  7481  r1elwf  7484  rankidb  7488  rankonidlem  7516  fseqenlem2  7668  dfac12lem1  7785  dfac12lem2  7786  pwsdompw  7846  ackbij2lem3  7883  ackbij2  7885  cfsmolem  7912  isfin4-3  7957  hsmexlem4  8071  ttukeylem3  8154  ttukeylem7  8158  iundom2g  8178  fpwwe2lem9  8276  canthwelem  8288  pwfseqlem4  8300  winalim2  8334  r1wunlim  8375  tskmid  8478  iccf1o  10794  fzopth  10844  fzoss2  10913  fzosubel3  10926  fzoend  10930  fzofzp1  10932  fzofzp1b  10933  peano2fzor  10935  zmodfzo  11008  seqf1olem2  11102  bcn2  11347  ccatval3  11449  swrdccat2  11477  splfv1  11486  wrdeqcats1  11490  revcl  11495  revlen  11496  revccat  11500  revrev  11501  revco  11505  limsupgre  11971  summolem2a  12204  fsumm1  12232  fsumcom2  12253  prmreclem4  12982  prmreclem5  12983  vdwapid1  13038  vdwlem5  13048  vdwlem8  13051  vdwnnlem2  13059  ramub1lem1  13089  ramub1lem2  13090  mrieqvlemd  13547  mreexd  13560  mreexexlemd  13562  catcocl  13603  catass  13604  moni  13655  epii  13662  inviso1  13684  episect  13699  subccocl  13735  fullsubc  13740  funcco  13761  cofucl  13778  resf2nd  13785  funcres  13786  fthepi  13818  nati  13845  arwhoma  13893  catccatid  13950  resscatc  13953  catcisolem  13954  catcoppccl  13956  catcfuccl  13957  xpcco  13973  xpcco2  13977  xpccatid  13978  prfcl  13993  catcxpccl  13997  curf12  14017  curf1cl  14018  curf2  14019  curf2cl  14021  curfcl  14022  uncf2  14027  uncfcurf  14029  diag12  14034  diag2  14035  curf2ndf  14037  hofcl  14049  oppchofcl  14050  oyoncl  14060  yonedalem3a  14064  yonedalem4b  14066  yonedalem22  14068  yonedalem3b  14069  yonedalem3  14070  yonedainv  14071  yonffthlem  14072  acsfiindd  14296  spwpr4  14356  spwpr4c  14357  mndpropd  14414  issubmnd  14417  imasmnd  14426  pwspjmhm  14460  gsumccat  14480  frmdmnd  14497  frmdgsum  14500  grpsubpropd2  14583  imasgrp  14627  subg0  14643  subgcl  14647  0ghm  14713  resghm2  14716  ghmco  14718  pwsdiagghm  14726  sylow1lem4  14928  sylow1lem5  14929  efglem  15041  efgtf  15047  efginvrel2  15052  efginvrel1  15053  efgsdmi  15057  efgs1b  15061  efgsres  15063  efgsfo  15064  efgredleme  15068  efgredlemc  15070  efgredlem  15072  efgcpbllemb  15080  frgp0  15085  frgpadd  15088  frgpinv  15089  vrgpf  15093  vrgpinv  15094  frgpuplem  15097  frgpup1  15100  frgpup2  15101  frgpup3lem  15102  frgpnabllem1  15177  frgpnabllem2  15178  gsumval3  15207  gsumzsubmcl  15216  dprdfid  15268  dprdsn  15287  dprd2da  15293  dpjidcl  15309  dpjghm  15314  pgpfac1lem2  15326  pgpfaclem3  15334  rngpropd  15388  imasrng  15418  divsrng2  15419  pwsco1rhm  15526  pwsco2rhm  15527  subrgmcl  15573  subrgunit  15579  issubdrg  15586  pwsdiagrhm  15594  isabvd  15601  lmodprop2d  15703  islssd  15709  prdsvscacl  15741  prdslmodd  15742  islmhm2  15811  lmhmco  15816  lmhmplusg  15817  lmhmvsca  15818  lmhmpropd  15842  lsppreli  15859  lspsnel4  15893  lssacsex  15913  lspsnat  15914  divs1  16003  divsrhm  16005  assapropd  16083  psrmulcllem  16148  psrvscacl  16154  psr0cl  16155  psrnegcl  16157  psr1cl  16163  resspsrmul  16177  subrgpsr  16179  mvrf  16185  mplmon  16223  mplcoe1  16225  subrgasclcl  16256  mplind  16259  subrgply1  16327  psrplusgpropd  16329  znf1o  16521  cssmre  16609  cldmreon  16847  maxlp  16894  ordttopon  16939  ordtrest2lem  16949  cnprcl2  16997  lmcnp  17048  resthauslem  17107  imacmp  17140  hauscmplem  17149  1stcfb  17187  2ndcctbss  17197  2ndcomap  17200  dis2ndc  17202  loclly  17229  hausllycmp  17236  kgeni  17248  kgenidm  17258  ptpjpre2  17291  xkoopn  17300  txopn  17313  ptpjopn  17322  ptcldmpt  17324  ptcls  17326  pthaus  17348  txkgen  17362  xkohaus  17363  xkopt  17365  txcon  17399  imastps  17428  kqid  17435  kqopn  17441  kqcld  17442  isr0  17444  indishmph  17505  pt1hmeo  17513  ptuncnv  17514  ptunhmeo  17515  t0kq  17525  filcon  17594  uzrest  17608  uffixsn  17636  fmfnfmlem2  17666  flimss2  17683  flimss1  17684  flimclslem  17695  flfcnp  17715  fclsfnflim  17738  uffclsflim  17742  fcfelbas  17747  alexsublem  17754  alexsub  17755  tmdgsum  17794  distgp  17798  indistgp  17799  symgtgp  17800  ghmcnp  17813  divstgpopn  17818  divstgplem  17819  divstgphaus  17821  prdstmdd  17822  prdstgpd  17823  tsmsid  17838  tsmssubm  17841  tsmsmhm  17844  tsmsadd  17845  tsmssplit  17850  blpnfctr  17998  lpbl  18065  met2ndci  18084  prdsxmslem2  18091  tmsxps  18098  metcnpi  18106  metcnpi2  18107  metcnpi3  18108  subgngp  18167  ngptgp  18168  sranlm  18211  nlmvscn  18214  nrginvrcn  18218  lssnlm  18227  nghmcn  18270  iccntr  18342  icccmplem2  18344  msdcn  18362  cncfmptc  18431  cncfmptid  18432  cncfmpt2f  18434  cnmpt2pc  18442  icoopnst  18453  iocopnst  18454  nmoleub2lem3  18612  nmoleub3  18616  nmhmcn  18617  ipcn  18689  cfilfcls  18716  caucfil  18725  equivcau  18742  caubl  18749  caublcls  18750  flimcfil  18755  minveclem3b  18808  minveclem4  18812  ovolicc2lem3  18894  ovolicc2lem4  18895  opnmbllem  18972  vitalilem2  18980  mbfsup  19035  mbfinf  19036  mbfi1fseqlem4  19089  limccnp  19257  limccnp2  19258  dvreslem  19275  dvres2lem  19276  dvidlem  19281  dvcnp2  19285  dvcn  19286  dvaddbr  19303  dvmulbr  19304  dvcmul  19309  dvcof  19313  dvcnvlem  19339  dvef  19343  rollelem  19352  dvlip2  19358  dvivthlem1  19371  dvivth  19373  lhop2  19378  lhop  19379  dvcnvrelem1  19380  dvcnvrelem2  19381  dvcnvre  19382  evlslem1  19415  evl1val  19427  evl1rhm  19428  pf1ind  19454  ply1rem  19565  fta1blem  19570  plycpn  19685  plyrem  19701  tayl0  19757  dvtaylp  19765  dvntaylp  19766  dvntaylp0  19767  taylthlem1  19768  taylthlem2  19769  ulmdvlem3  19795  psercn  19818  pserdv  19821  abelth  19833  efopnlem1  20019  loglesqr  20114  efrlim  20280  dchrghm  20511  dchrptlem3  20521  spansnid  22158  elspansn4  22168  ballotlemrv  23094  gsumpropd2lem  23394  esumel  23441  esumsplit  23446  elsx  23540  dya2iocseg  23594  dstfrvel  23689  subfacp1lem5  23730  ptpcon  23779  indispcon  23780  cvxscon  23789  cvmseu  23822  cvmliftmolem2  23828  cvmliftlem7  23837  cvmliftlem10  23840  cvmliftlem13  23842  cvmlift2lem12  23860  vdgr1d  23909  vdgr1b  23910  eupap1  23915  prodmolem2a  24157  predfz  24274  linerflx1  24844  linerflx2  24846  elhf2  24877  areacirclem4  25030  areacirclem5  25032  npincppr  25262  clfsebsr  25452  mapdiscn  25630  mapudiscn  25631  rcmob  25852  rocatval  26062  empklst  26112  lineval2a  26188  sgplpte21d1  26242  locfincmp  26407  neibastop2lem  26412  blssp  26573  sstotbnd2  26601  totbndbnd  26616  prdstotbnd  26621  cnpwstotbnd  26624  heiborlem9  26646  exidcl  26669  exidresid  26672  grpokerinj  26678  iscringd  26727  prter3  26853  wepwsolem  27241  kelac1  27264  kercvrlsm  27284  dsmmlss  27313  frlmsplit2  27346  frlmup1  27353  dfacbasgrp  27376  en1uniel  27483  psgnunilem1  27519  psgnunilem5  27520  psgnunilem2  27521  psgnunilem3  27522  matbas2i  27579  matplusg2  27580  matvsca2  27581  cntzsdrg  27613  dvconstbi  27654  fnchoice  27803  cncmpmax  27806  climsuse  27837  stoweidlem26  27878  stoweidlem34  27886  stoweidlem59  27911  eldmressnsn  28089  nbgraop  28274  bnj1006  29307  bnj1018  29310  bnj1121  29331  bnj1398  29380  bnj1450  29396  bnj1501  29413  toycom  29784  islfld  29874  lshpsmreu  29921  ldualelvbase  29939  ldualssvscl  29970  lkreqN  29982  lkrlspeqN  29983  erng1lem  31798  erngdvlem4  31802  erng0g  31805  erng1r  31806  erngdvlem4-rN  31810  dva0g  31839  dia1dim2  31874  dia1dimid  31875  dia2dimlem5  31880  dvhelvbasei  31900  dvhvaddass  31909  tendoinvcl  31916  tendolinv  31917  tendorinv  31918  dvhgrp  31919  dvhlveclem  31920  diblss  31982  cdlemn4  32010  lcfrlem12N  32366  lcfrlem15  32369  lcdvscl  32417  lcdlssvscl  32418  lcdvsass  32419  lcdvs0N  32428  mapdincl  32473  mapdin  32474  mapdlsmcl  32475  mapdcnvatN  32478  mapdpglem2  32485  mapdpglem12  32495  mapdpglem18  32501  mapdpglem21  32504  mapdpglem22  32505  mapdpglem28  32513  mapdpglem30  32514  hdmaprnlem3N  32665  hdmaprnlem3uN  32666  hdmaprnlem7N  32670  hdmaprnlem8N  32671  hdmaprnlem9N  32672  hdmaprnlem3eN  32673  hdmaprnlem16N  32677  hgmapdcl  32705  hgmapval1  32708  hgmaprnlem4N  32714  hdmapinvlem1  32733
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator