Theorem eleqtrd 2551

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 2534	. 2 |- ( ph -> ( A e. B <-> A e. C ) )
4	1, 3	mpbid 215	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1452   e. wcel 1904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-cleq 2464  df-clel 2467

This theorem is referenced by:  eleqtrrd  2552  syl5eleq  2555  syl6eleq  2559  3eltr3d  2563  opth1  4675  0nelop  4691  fviss  5938  tfisi  6704  fnwelem  6930  wfrlem17  7070  omeulem1  7301  oeeulem  7320  oeeui  7321  oaabs2  7364  omabs  7366  ercl  7392  erth  7426  ecelqsdm  7451  ordtypelem6  8056  ordtypelem7  8057  cantnfval  8191  cantnfp1lem3  8203  cantnflem4  8215  r1pwss  8273  rankonidlem  8317  rankxplim3  8370  fseqenlem2  8474  iunfictbso  8563  dfac12lem1  8591  dfac12lem2  8592  fin23lem30  8790  iundom2g  8983  fpwwe2lem6  9078  fpwwe2lem9  9081  lincmb01cmp  11801  fzopth  11861  fzoaddel2  11999  fzosubel2  12003  fzocatel  12007  zpnn0elfzo1  12016  fzoend  12031  peano2fzor  12047  monoord2  12282  sermono  12283  expmulnbnd  12442  bcpasc  12544  swrdcl  12829  revcl  12920  revlen  12921  fsum0diag2  13921  isumsplit  13975  fprodser  14080  sadadd  14520  sadass  14524  smuval2  14535  smumul  14546  vdwapun  15003  vdwlem9  15018  ramub1lem1  15063  prdsbasfn  15447  prdsbasprj  15448  pwsplusgval  15466  pwsmulrval  15467  pwsvscafval  15470  xpsaddlem  15559  xpsvsca  15563  xpsle  15565  mreexmrid  15627  homfeqval  15680  comfval2  15686  comfeq  15689  comfeqval  15691  oppccomfpropd  15710  invco  15754  sectepi  15767  issubc3  15832  funcf2  15851  funciso  15857  fthepi  15911  nat1st2nd  15934  fuciso  15958  homarcl2  16008  coapm  16044  setcmon  16060  setcepi  16061  setcsect  16062  setcinv  16063  setciso  16064  catccatid  16075  resscatc  16078  catciso  16080  catcoppccl  16081  catcfuccl  16082  xpccatid  16151  catcxpccl  16170  xpcpropd  16171  evlfcl  16185  curfpropd  16196  hofcl  16222  yonedalem3  16243  yonffthlem  16245  poslubdg  16473  grpidd  16589  gsumress  16597  ismndd  16637  mndpropd  16640  issubmnd  16642  submnd0  16644  imasmnd  16652  frmdelbas  16715  grpidd2  16781  submmulg  16871  pwsinvg  16876  imasgrp  16880  subginvcl  16904  subgcl  16905  subgsub  16907  subgmulg  16909  quseccl  16951  gaid2  17035  submod  17296  odsubdvds  17298  sylow1lem4  17331  sylow2alem2  17348  lsmdisj2  17410  subgdisj1  17419  pj1id  17427  efgsrel  17462  efgrelexlemb  17478  efgcpbl2  17485  frgpcpbl  17487  frgp0  17488  frgpeccl  17489  frgpadd  17491  frgpup3lem  17505  frgpnabllem1  17587  cycsubgcyg  17613  prdsgsum  17688  dprdfeq0  17733  dmdprdsplitlem  17748  dpjidcl  17769  pgpfac1lem3a  17787  pgpfac1lem4  17789  pgpfaclem1  17792  pgpfaclem2  17793  ablfaclem2  17797  ringidss  17885  ringpropd  17890  imasring  17925  qusring2  17926  kerf1hrm  18049  subrg1  18096  subrgmcl  18098  subrgdv  18103  subrgunit  18104  issubdrg  18111  resrhm  18115  lmodprop2d  18228  0lmhm  18341  lmhmpropd  18374  lspfixed  18429  lssacsex  18445  lbsextlem4  18462  quscrng  18541  assapropd  18628  psrelbas  18680  resspsrvsca  18719  subrgpsr  18720  mplcoe1  18766  mplbas2  18771  mplascl  18796  mplmon2cl  18800  mplmon2mul  18801  evlrhm  18825  mpfconst  18830  vr1cl2  18863  ply1lss  18866  ply1subrg  18867  psropprmul  18908  evl1vsd  19009  evl1expd  19010  evl1gsumadd  19023  evl1gsummon  19030  znf1o  19199  psgnghm2  19226  elocv  19308  pjff  19352  frlmlss  19391  frlmsubgval  19404  frlmvscafval  19405  frlmphl  19416  uvcresum  19428  frlmssuvc1  19429  frlmssuvc2  19430  frlmsslsp  19431  frlmup1  19433  matring  19545  matassa  19546  mat1  19549  mattposcl  19555  mavmulass  19651  mdetunilem9  19722  matinv  19779  cpmadugsumlemF  19977  cpmadugsumfi  19978  cpmidgsum2  19980  elcls3  20176  mreclatdemoBAD  20189  neiptopnei  20225  resstps  20280  ordtrest2lem  20296  ordtrest2  20297  pnfnei  20313  mnfnei  20314  iscnp2  20332  iscnp4  20356  cnrest2r  20380  lmcls  20395  lmcld  20396  cnt0  20439  cnhaus  20447  isreg2  20470  conclo  20507  1stccnp  20554  loclly  20579  lly1stc  20588  locfincmp  20618  unisngl  20619  comppfsc  20624  kgencmp2  20638  llycmpkgen2  20642  kgen2ss  20647  kgencn3  20650  pttoponconst  20689  txcls  20696  txbasval  20698  dfac14lem  20709  ptcn  20719  ptrescn  20731  txtube  20732  txcmplem1  20733  txlm  20740  txkgen  20744  xkopjcn  20748  cnmptkp  20772  xkoinjcn  20779  qtopkgen  20802  imastps  20813  isr0  20829  r0cld  20830  pt1hmeo  20898  ptuncnv  20899  ptunhmeo  20900  filintn0  20954  trnei  20985  flimfil  21062  flimopn  21068  fbflim2  21070  cnpflf2  21093  flfcnp  21097  flfcnp2  21100  fclsopn  21107  fcfnei  21128  cnpfcf  21134  flfcntr  21136  alexsublem  21137  ptcmplem3  21147  ptcmplem4  21148  cnextfres1  21161  tmdcn2  21182  tmdgsum  21188  tmdgsum2  21189  symgtgp  21194  tgphaus  21209  tgpt1  21210  qustgplem  21213  prdstmdd  21216  prdstgpd  21217  haustsms  21228  tsmscls  21230  tsmsmhm  21238  tsmsadd  21239  tgptsmscls  21242  tsmssplit  21244  restutop  21330  utopreg  21345  ressusp  21358  ucncn  21378  xmetunirn  21430  ressprdsds  21464  xpsdsval  21474  xblss2ps  21494  blbas  21523  mopntopon  21532  isxms2  21541  imasf1oxms  21582  imasf1oms  21583  prdsxmslem2  21622  tmsxpsval  21631  tngngp2  21738  tngngp  21740  tgioo  21892  metdseq0  21949  metdseq0OLD  21964  cncfmpt2f  22024  cncfcnvcn  22031  cnmptre  22033  cnheibor  22061  nmhmcn  22212  cvsdiv  22218  cvsdivcl  22219  cphsubrglem  22233  cphreccllem  22234  iscmet3  22341  relcmpcmet  22364  bcthlem4  22373  rrxds  22430  minveclem4  22452  minveclem4OLD  22464  ivthicc  22487  evthicc  22488  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ovolicc2lem5  22553  iunmbl2  22589  vitalilem3  22647  cncombf  22693  cnmbf  22694  dvres2lem  22944  cpncn  22969  cpnres  22970  dvaddbr  22971  dvmulbr  22972  dvcobr  22979  dvcjbr  22982  dvrec  22988  dvcnvlem  23007  dvlip2  23026  dvivth  23041  lhop2  23046  lhop  23047  dvcnvrelem1  23048  dvcnvrelem2  23049  dvcnvre  23050  ftc1lem6  23072  mdegvscale  23103  mdegvsca  23104  fta1blem  23198  plyaddlem1  23246  plymullem1  23247  coeeulem  23257  tayl0  23396  taylthlem1  23407  taylthlem2  23408  ulmdvlem3  23436  psercnlem2  23458  psercn  23460  efsubm  23579  cxpcn3  23767  loglesqrt  23777  efrlim  23974  ppinprm  24158  chtnprm  24160  dchrptlem1  24271  dchrptlem2  24272  tgbtwnouttr2  24618  tgldim0eq  24626  tgifscgr  24632  iscgrglt  24638  ercgrg  24641  tgcgrxfr  24642  motcgrg  24668  tglngne  24674  tgcolg  24678  tgbtwnconn1lem2  24697  tgbtwnconn1lem3  24698  legtri3  24714  legbtwn  24718  ncolne1  24749  tgisline  24751  tglinethru  24760  coltr3  24772  colline  24773  tglowdim2ln  24775  mirinv  24790  miriso  24794  mirauto  24808  miduniq  24809  krippenlem  24814  midexlem  24816  ragperp  24841  footex  24842  perpdragALT  24848  perpdrag  24849  colperpexlem1  24851  colperpexlem3  24853  mideulem2  24855  midex  24858  opphllem1  24868  opphllem3  24870  opphllem4  24871  hlpasch  24877  trgcopy  24925  acopyeu  24954  f1otrg  24980  axlowdimlem16  25066  elntg  25093  eengtrkg  25094  eengtrkge  25095  eupap1  25783  grpoidinv2  26027  grpoinv  26036  ubthlem2  26594  shuni  27034  acunirnmpt  28336  acunirnmpt2  28337  acunirnmpt2f  28338  fpwrelmap  28393  gsummpt2d  28618  rngurd  28625  ordtrest2NEWlem  28802  ordtrest2NEW  28803  lmxrge0  28832  nmmulg  28846  rrhcn  28875  esumadd  28952  esumaddf  28956  esumcocn  28975  measiuns  29113  mbfmco2  29160  dya2iocnrect  29176  omscl  29192  omsf  29193  omsclOLD  29196  omsfOLD  29197  oms0  29198  oms0OLD  29202  sibf0  29240  sibfof  29246  sitgaddlemb  29254  fibp1  29307  ccatmulgnn0dir  29500  bnj1450  29931  bnj1501  29948  indispcon  30029  conpcon  30030  pconpi1  30032  sconpi1  30034  cvmsss2  30069  cvmliftmolem1  30076  cvmliftlem8  30087  cvmliftlem10  30089  cvmliftlem11  30090  cvmlift2lem9  30106  cvmlift2lem12  30109  cvmlift3lem7  30120  mrsubcv  30220  mrsubff  30222  mrsubccat  30228  elmrsubrn  30230  mrsubco  30231  mrsubvrs  30232  linethru  30991  ivthALT  31062  neibastop2  31088  filnetlem4  31108  poimirlem1  32005  poimirlem2  32006  poimirlem8  32012  poimirlem9  32013  poimirlem16  32020  poimirlem17  32021  poimirlem19  32023  poimirlem20  32024  poimirlem22  32026  poimirlem23  32027  poimir  32037  broucube  32038  areacirclem4  32099  fdc  32138  isbnd3  32180  prdsbnd  32189  prdstotbnd  32190  prdsbnd2  32191  rrnequiv  32231  reheibor  32235  iscringd  32296  isfldidl  32365  eqlkr  32736  ldualvsubval  32794  dvalveclem  34664  dia2dimlem5  34707  dia2dimlem9  34711  tendoinvcl  34743  dvhgrp  34746  dvhlveclem  34747  dihpN  34975  dochsnkr2cl  35113  lcfl7lem  35138  lclkr  35172  lclkrs  35178  lcfrvalsnN  35180  lcfrlem4  35184  lcfrlem6  35186  lcfrlem16  35197  lcdvsubval  35257  lcdlkreqN  35261  mapdcl2  35295  mapdincl  35300  mapdlsmcl  35302  mapdpglem3  35314  hdmaprnlem9N  35499  hdmaplkr  35555  hdmapip0  35557  hdmapglem7a  35569  diophin  35686  acongeq  35904  isnumbasgrplem2  36034  proot1mul  36144  iunrelexpuztr  36382  bccbc  36764  suctrALT  37285  disjf1o  37537  disjinfi  37539  choicefi  37552  fsneq  37558  fsneqrn  37564  unirnmapsn  37567  iunmapsn  37570  monoords  37602  elfzolem1  37631  uzfissfz  37636  evthiccabs  37689  iooabslt  37692  islptre  37796  limciccioolb  37798  sumnnodd  37807  limcicciooub  37814  lptre2pt  37817  limcresiooub  37820  limcresioolb  37821  lptioo1cn  37824  reclimc  37831  fsumcncf  37852  ioccncflimc  37860  cncfuni  37861  icccncfext  37862  cncficcgt0  37863  icocncflimc  37864  cncfdmsn  37865  cncfiooicclem1  37868  cncfiooicc  37869  cncfioobd  37872  cxpcncf2  37875  fperdvper  37887  dvcosax  37895  dvnmul  37915  dvnprodlem1  37918  dvnprodlem2  37919  itgsubsticclem  37949  fvvolioof  37964  fvvolicof  37966  stoweidlem26  37998  stoweidlem27  37999  stoweidlem31  38004  stoweidlem34  38007  dirkercncflem2  38078  dirkercncflem3  38079  dirkercncflem4  38080  dirkercncf  38081  fourierdlem16  38097  fourierdlem20  38101  fourierdlem21  38102  fourierdlem22  38103  fourierdlem26  38107  fourierdlem32  38114  fourierdlem33  38115  fourierdlem38  38120  fourierdlem39  38121  fourierdlem46  38128  fourierdlem48  38130  fourierdlem49  38131  fourierdlem53  38135  fourierdlem60  38142  fourierdlem61  38143  fourierdlem69  38151  fourierdlem70  38152  fourierdlem71  38153  fourierdlem73  38155  fourierdlem74  38156  fourierdlem75  38157  fourierdlem76  38158  fourierdlem80  38162  fourierdlem81  38163  fourierdlem82  38164  fourierdlem83  38165  fourierdlem84  38166  fourierdlem85  38167  fourierdlem88  38170  fourierdlem89  38171  fourierdlem91  38173  fourierdlem92  38174  fourierdlem93  38175  fourierdlem100  38182  fourierdlem101  38183  fourierdlem103  38185  fourierdlem104  38186  fourierdlem107  38189  fourierdlem111  38193  fourierdlem112  38194  fourierdlem113  38195  fouriersw  38207  fouriercn  38208  etransclem24  38235  etransclem26  38237  etransclem28  38239  etransclem31  38242  etransclem32  38243  etransclem33  38244  etransclem34  38245  etransclem35  38246  etransclem38  38249  rrxbasefi  38264  rrxdsfi  38266  rrxtopnfi  38267  rrxmetfi  38268  rrxtoponfi  38272  qndenserrnbl  38276  qndenserrnopnlem  38278  qndenserrn  38280  prsal  38291  intsaluni  38300  salgencntex  38314  fge0iccico  38326  sge0sn  38335  sge0tsms  38336  sge0cl  38337  sge0f1o  38338  sge0pr  38350  sge0isum  38383  nnfoctbdjlem  38409  iundjiunlem  38413  iundjiun  38414  meadjiunlem  38419  psmeasure  38425  caragenelss  38441  omeunile  38445  carageniuncllem1  38461  carageniuncllem2  38462  0ome  38469  isomenndlem  38470  isomennd  38471  hoicvr  38488  ovnpnfelsup  38499  ovncvrrp  38504  ovnsubaddlem1  38510  hoidmv1le  38534  hoidmvlelem2  38536  hoidmvlelem3  38537  hoidmvlelem4  38538  hoidmvle  38540  ovnhoilem1  38541  hoi2toco  38547  ovncvr2  38551  hspdifhsp  38556  voncmpl  38561  hoiqssbl  38565  hspmbllem2  38567  hspmbl  38569  hoimbllem  38570  opnvonmbllem2  38573  mblvon  38579  ovolval3  38587  ovolval4lem1  38589  ovnovollem1  38596  ovnovollem2  38597  fzoopth  39208  issubmgm2  40298  zlmodzxzel  40644  ply1mulgsum  40690