Theorem eleqtrd 2533

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrd.1	|- ( ph -> A e. B )
eleqtrd.2	|- ( ph -> B = C )

Assertion

Ref	Expression
eleqtrd	|- ( ph -> A e. C )

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 |- ( ph -> A e. B )
2		eleqtrd.2	. . 3 |- ( ph -> B = C )
3	2	eleq2d 2513	. 2 |- ( ph -> ( A e. B <-> A e. C ) )
4	1, 3	mpbid 210	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1383   e. wcel 1804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-cleq 2435  df-clel 2438

This theorem is referenced by:  eleqtrrd  2534  syl5eleq  2537  syl6eleq  2541  3eltr3d  2545  opth1  4710  0nelop  4727  fviss  5916  tfisi  6678  fnwelem  6900  omeulem1  7233  oeeulem  7252  oeeui  7253  oaabs2  7296  omabs  7298  ercl  7324  erth  7358  ecelqsdm  7383  ordtypelem6  7951  ordtypelem7  7952  cantnfval  8090  cantnfp1lem3  8102  cantnflem4  8114  cantnfvalOLD  8120  cantnfp1lem3OLD  8128  cantnflem4OLD  8136  r1pwss  8205  rankonidlem  8249  rankxplim3  8302  fseqenlem2  8409  iunfictbso  8498  dfac12lem1  8526  dfac12lem2  8527  fin23lem30  8725  iundom2g  8918  fpwwe2lem6  9016  fpwwe2lem9  9019  lincmb01cmp  11673  fzopth  11730  fzoaddel2  11855  fzosubel2  11857  fzocatel  11861  zpnn0elfzo1  11870  fzoend  11884  peano2fzor  11898  monoord2  12119  sermono  12120  expmulnbnd  12279  bcpasc  12380  ccatcl  12574  ccatw2s1p2  12622  swrdcl  12627  revcl  12716  revlen  12717  fsum0diag2  13579  isumsplit  13633  fprodser  13737  sadadd  14098  sadass  14102  smuval2  14113  smumul  14124  vdwapun  14473  vdwlem9  14488  ramub1lem1  14525  prdsbasfn  14849  prdsbasprj  14850  pwsplusgval  14868  pwsmulrval  14869  pwsvscafval  14872  xpsaddlem  14953  xpsvsca  14957  xpsle  14959  mreexmrid  15021  homfeqval  15073  comfval2  15079  comfeq  15082  comfeqval  15084  oppccomfpropd  15103  invco  15146  sectepi  15155  issubc3  15196  funcf2  15215  funciso  15221  fthepi  15275  nat1st2nd  15298  fuciso  15322  homarcl2  15340  coapm  15376  setcmon  15392  setcepi  15393  setcsect  15394  setcinv  15395  setciso  15396  catccatid  15407  resscatc  15410  catciso  15412  catcoppccl  15413  catcfuccl  15414  xpccatid  15435  catcxpccl  15454  xpcpropd  15455  evlfcl  15469  curfpropd  15480  hofcl  15506  yonedalem3  15527  yonffthlem  15529  poslubdg  15757  grpidd  15873  gsumress  15881  ismndd  15921  mndpropd  15924  issubmnd  15926  submnd0  15928  imasmnd  15936  frmdelbas  15999  grpidd2  16065  submmulg  16155  pwsinvg  16160  imasgrp  16164  subginvcl  16188  subgcl  16189  subgsub  16191  subgmulg  16193  quseccl  16235  gaid2  16319  submod  16567  odsubdvds  16569  sylow1lem4  16599  sylow2alem2  16616  lsmdisj2  16678  subgdisj1  16687  pj1id  16695  efgsrel  16730  efgrelexlemb  16746  efgcpbl2  16753  frgpcpbl  16755  frgp0  16756  frgpeccl  16757  frgpadd  16759  frgpup3lem  16773  frgpnabllem1  16855  cycsubgcyg  16881  prdsgsum  16985  prdsgsumOLD  16986  dprdfeq0  17040  dprdfeq0OLD  17047  dmdprdsplitlem  17062  dmdprdsplitlemOLD  17063  dpjidcl  17085  dpjidclOLD  17092  pgpfac1lem3a  17105  pgpfac1lem4  17107  pgpfaclem1  17110  pgpfaclem2  17111  ablfaclem2  17115  ringidss  17203  ringpropd  17208  imasring  17246  qusring2  17247  kerf1hrm  17370  subrg1  17417  subrgmcl  17419  subrgdv  17424  subrgunit  17425  issubdrg  17432  resrhm  17436  lmodprop2d  17550  0lmhm  17664  lmhmpropd  17697  lspfixed  17752  lssacsex  17768  lbsextlem4  17785  quscrng  17866  assapropd  17954  psrelbas  18010  resspsrvsca  18051  subrgpsr  18052  mplcoe1  18105  mplbas2  18112  mplbas2OLD  18113  mplascl  18139  mplmon2cl  18143  mplmon2mul  18144  evlrhm  18172  mpfconst  18177  vr1cl2  18210  ply1lss  18213  ply1subrg  18214  psropprmul  18257  evl1vsd  18358  evl1expd  18359  evl1gsumadd  18372  evl1gsummon  18379  znf1o  18567  psgnghm2  18594  elocv  18676  pjff  18720  frlmlss  18759  frlmsubgval  18775  frlmvscafval  18776  frlmphl  18789  uvcresum  18801  frlmssuvc1  18802  frlmssuvc2  18803  frlmssuvc1OLD  18804  frlmssuvc2OLD  18805  frlmsslsp  18806  frlmsslspOLD  18807  frlmup1  18809  matring  18922  matassa  18923  mat1  18926  mattposcl  18932  mavmulass  19028  mdetunilem9  19099  matinv  19156  cpmadugsumlemF  19354  cpmadugsumfi  19355  cpmidgsum2  19357  elcls3  19561  mreclatdemoBAD  19574  neiptopnei  19610  resstps  19665  ordtrest2lem  19681  ordtrest2  19682  pnfnei  19698  mnfnei  19699  iscnp2  19717  iscnp4  19741  cnrest2r  19765  lmcls  19780  lmcld  19781  cnt0  19824  cnhaus  19832  isreg2  19855  conclo  19893  1stccnp  19940  loclly  19965  lly1stc  19974  locfincmp  20004  unisngl  20005  comppfsc  20010  kgencmp2  20024  llycmpkgen2  20028  kgen2ss  20033  kgencn3  20036  pttoponconst  20075  txcls  20082  txbasval  20084  dfac14lem  20095  ptcn  20105  ptrescn  20117  txtube  20118  txcmplem1  20119  txlm  20126  txkgen  20130  xkopjcn  20134  cnmptkp  20158  xkoinjcn  20165  qtopkgen  20188  imastps  20199  isr0  20215  r0cld  20216  pt1hmeo  20284  ptuncnv  20285  ptunhmeo  20286  filintn0  20339  trnei  20370  flimfil  20447  flimopn  20453  fbflim2  20455  cnpflf2  20478  flfcnp  20482  flfcnp2  20485  fclsopn  20492  fcfnei  20513  cnpfcf  20519  alexsublem  20521  ptcmplem3  20531  ptcmplem4  20532  cnextfres  20545  tmdcn2  20565  tmdgsum  20571  tmdgsum2  20572  symgtgp  20577  tgphaus  20592  tgpt1  20593  qustgplem  20596  prdstmdd  20599  prdstgpd  20600  haustsms  20611  tsmscls  20613  tsmsmhm  20625  tsmsadd  20626  tgptsmscls  20629  tsmssplit  20631  restutop  20717  utopreg  20732  ressusp  20745  ucncn  20765  xmetunirn  20817  ressprdsds  20851  xpsdsval  20861  xblss2ps  20881  blbas  20910  mopntopon  20919  isxms2  20928  imasf1oxms  20969  imasf1oms  20970  prdsxmslem2  21009  tmsxpsval  21018  tngngp2  21143  tngngp  21145  tgioo  21278  metdseq0  21335  cncfmpt2f  21395  cncfcnvcn  21402  cnmptre  21404  cnheibor  21432  nmhmcn  21580  cvsdiv  21586  cvsdivcl  21587  cphsubrglem  21601  cphreccllem  21602  iscmet3  21709  relcmpcmet  21732  bcthlem4  21743  rrxds  21802  minveclem4  21824  ivthicc  21847  evthicc  21848  ovolicc2lem4  21908  ovolicc2lem5  21909  iunmbl2  21944  vitalilem3  21996  cncombf  22042  cnmbf  22043  dvres2lem  22291  cpncn  22316  cpnres  22317  dvaddbr  22318  dvmulbr  22319  dvcobr  22326  dvcjbr  22329  dvrec  22335  dvcnvlem  22354  dvlip2  22373  dvivth  22388  lhop2  22393  lhop  22394  dvcnvrelem1  22395  dvcnvrelem2  22396  dvcnvre  22397  ftc1lem6  22419  mdegvscale  22452  mdegvsca  22453  fta1blem  22546  plyaddlem1  22587  plymullem1  22588  coeeulem  22598  tayl0  22733  taylthlem1  22744  taylthlem2  22745  ulmdvlem3  22773  psercnlem2  22795  psercn  22797  efsubm  22914  cxpcn3  23098  loglesqrt  23108  efrlim  23275  ppinprm  23402  chtnprm  23404  dchrptlem1  23515  dchrptlem2  23516  tgbtwnouttr2  23862  tgldim0eq  23870  tgifscgr  23876  ercgrg  23884  tgcgrxfr  23885  motcgrg  23907  tglngne  23913  tgcolg  23917  tgbtwnconn1lem2  23936  tgbtwnconn1lem3  23937  legtri3  23953  legbtwn  23957  ncolne1  23981  tgisline  23983  tglinethru  23992  coltr3  24005  colline  24006  tglowdim2ln  24008  mirinv  24023  miriso  24026  mirauto  24037  miduniq  24038  krippenlem  24043  midexlem  24045  ragperp  24070  footex  24071  perpdragALT  24077  perpdrag  24078  colperpexlem1  24080  colperpexlem3  24082  mideulem2  24084  midex  24087  opphllem1  24095  opphllem3  24097  opphllem4  24098  f1otrg  24150  axlowdimlem16  24236  elntg  24263  eengtrkg  24264  eengtrkge  24265  eupap1  24952  grpoidinv2  25196  grpoinv  25205  ubthlem2  25763  shuni  26194  fpwrelmap  27532  rngurd  27755  ordtrest2NEWlem  27881  ordtrest2NEW  27882  lmxrge0  27911  nmmulg  27926  rrhcn  27955  esumadd  28041  esumaddf  28046  esumcocn  28063  measiuns  28165  mbfmco2  28213  dya2iocnrect  28229  oms0  28243  sibf0  28253  sibfof  28259  fibp1  28317  ccatmulgnn0dir  28473  indispcon  28656  conpcon  28657  pconpi1  28659  sconpi1  28661  cvmsss2  28696  cvmliftmolem1  28703  cvmliftlem8  28714  cvmliftlem10  28716  cvmliftlem11  28717  cvmlift2lem9  28733  cvmlift2lem12  28736  cvmlift3lem7  28747  mrsubcv  28847  mrsubff  28849  mrsubccat  28855  elmrsubrn  28857  mrsubco  28858  mrsubvrs  28859  linethru  29778  areacirclem4  30085  ivthALT  30128  neibastop2  30154  filnetlem4  30174  fdc  30213  isbnd3  30255  prdsbnd  30264  prdstotbnd  30265  prdsbnd2  30266  rrnequiv  30306  reheibor  30310  iscringd  30371  isfldidl  30440  diophin  30681  acongeq  30896  isnumbasgrplem2  31028  proot1mul  31132  monoords  31445  evthiccabs  31465  iooabslt  31468  islptre  31533  limciccioolb  31535  sumnnodd  31544  limcicciooub  31551  lptre2pt  31554  limcresiooub  31556  limcresioolb  31557  lptioo1cn  31560  reclimc  31567  fsumcncf  31587  ioccncflimc  31595  cncfuni  31596  icccncfext  31597  cncficcgt0  31598  icocncflimc  31599  cncfdmsn  31600  cncfiooicclem1  31603  cncfiooicc  31604  cncfioobd  31607  fperdvper  31619  dvcosax  31627  itgsubsticclem  31664  stoweidlem26  31697  stoweidlem27  31698  stoweidlem31  31702  stoweidlem34  31705  dirkercncflem2  31775  dirkercncflem3  31776  dirkercncflem4  31777  dirkercncf  31778  fourierdlem16  31794  fourierdlem20  31798  fourierdlem21  31799  fourierdlem22  31800  fourierdlem26  31804  fourierdlem32  31810  fourierdlem33  31811  fourierdlem38  31816  fourierdlem39  31817  fourierdlem46  31824  fourierdlem48  31826  fourierdlem49  31827  fourierdlem53  31831  fourierdlem60  31838  fourierdlem61  31839  fourierdlem69  31847  fourierdlem70  31848  fourierdlem71  31849  fourierdlem73  31851  fourierdlem74  31852  fourierdlem75  31853  fourierdlem76  31854  fourierdlem80  31858  fourierdlem81  31859  fourierdlem82  31860  fourierdlem83  31861  fourierdlem84  31862  fourierdlem85  31863  fourierdlem88  31866  fourierdlem89  31867  fourierdlem91  31869  fourierdlem92  31870  fourierdlem93  31871  fourierdlem100  31878  fourierdlem101  31879  fourierdlem103  31881  fourierdlem104  31882  fourierdlem107  31885  fourierdlem111  31889  fourierdlem112  31890  fourierdlem113  31891  fouriersw  31903  fouriercn  31904  el2fzo  32177  fzoopth  32178  issubmgm2  32316  zlmodzxzel  32677  ply1mulgsum  32725  suctrALT  33359  bnj1450  33839  bnj1501  33856  eqlkr  34564  ldualvsubval  34622  dvalveclem  36492  dia2dimlem5  36535  dia2dimlem9  36539  tendoinvcl  36571  dvhgrp  36574  dvhlveclem  36575  dihpN  36803  dochsnkr2cl  36941  lcfl7lem  36966  lclkr  37000  lclkrs  37006  lcfrvalsnN  37008  lcfrlem4  37012  lcfrlem6  37014  lcfrlem16  37025  lcdvsubval  37085  lcdlkreqN  37089  mapdcl2  37123  mapdincl  37128  mapdlsmcl  37130  mapdpglem3  37142  hdmaprnlem9N  37327  hdmaplkr  37383  hdmapip0  37385  hdmapglem7a  37397