Theorem eleqtrd 2915

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

Hypotheses

Ref	Expression
eleqtrd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eleqtrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eleq2d 2898	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 234	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  eleqtrrd  2916  eleqtrid  2919  eleqtrdi  2923  3eltr3d  2927  prel12g  4794  opth1  5367  0nelop  5386  fvelimad  6732  fviss  6741  tfisi  7573  fnwelem  7825  wfrlem17  7971  omeulem1  8208  oeeulem  8227  oeeui  8228  oaabs2  8272  omabs  8274  ercl  8300  erth  8338  ecelqsdm  8367  ordtypelem6  8987  ordtypelem7  8988  cantnfval  9131  cantnfp1lem3  9143  cantnflem4  9155  r1pwss  9213  rankonidlem  9257  rankxplim3  9310  fseqenlem2  9451  iunfictbso  9540  dfac12lem1  9569  dfac12lem2  9570  fin23lem30  9764  iundom2g  9962  fpwwe2lem6  10057  fpwwe2lem9  10060  lincmb01cmp  12882  fzopth  12945  fzoaddel2  13094  fzosubel2  13098  fzocatel  13102  zpnn0elfzo1  13112  fzoend  13129  peano2fzor  13145  monoord2  13402  sermono  13403  expmulnbnd  13597  bcpasc  13682  hash1elsn  13733  swrdcl  14007  revcl  14123  revlen  14124  fsum0diag2  15138  isumsplit  15195  fprodser  15303  sadadd  15816  sadass  15820  smuval2  15831  smumul  15842  vdwapun  16310  vdwlem9  16325  ramub1lem1  16362  prdsbasfn  16744  prdsbasprj  16745  pwsplusgval  16763  pwsmulrval  16764  pwsvscafval  16767  xpsaddlem  16846  xpsvsca  16850  xpsle  16852  mreexmrid  16914  homfeqval  16967  comfval2  16973  comfeq  16976  comfeqval  16978  oppccomfpropd  16997  invco  17041  sectepi  17054  issubc3  17119  funcf2  17138  fthepi  17198  nat1st2nd  17221  homarcl2  17295  coapm  17331  setcmon  17347  setcepi  17348  setcsect  17349  setcinv  17350  setciso  17351  catccatid  17362  resscatc  17365  catciso  17367  catcoppccl  17368  catcfuccl  17369  xpccatid  17438  catcxpccl  17457  xpcpropd  17458  evlfcl  17472  curfpropd  17483  hofcl  17509  yonedalem3  17530  yonffthlem  17532  poslubdg  17759  grpidd  17881  gsumress  17892  ismndd  17933  mndpropd  17936  issubmnd  17938  submnd0  17940  imasmnd  17949  frmdelbas  18018  grpidd2  18141  pwsinvg  18212  imasgrp  18215  submmulg  18271  subginvcl  18288  subgcl  18289  subgsub  18291  subgmulg  18293  1nsgtrivd  18326  quseccl  18336  gaid2  18433  submod  18694  odsubdvds  18696  sylow1lem4  18726  sylow2alem2  18743  lsmdisj2  18808  subgdisj1  18817  pj1id  18825  efgsrel  18860  efgrelexlemb  18876  efgcpbl2  18883  frgpcpbl  18885  frgp0  18886  frgpeccl  18887  frgpadd  18889  frgpup3lem  18903  frgpnabllem1  18993  cycsubgcyg  19021  prdsgsum  19101  dprdfeq0  19144  dmdprdsplitlem  19159  dpjidcl  19180  pgpfac1lem3a  19198  pgpfac1lem4  19200  pgpfaclem1  19203  pgpfaclem2  19204  ablfaclem2  19208  simpgnsgeqd  19223  simpgnsgbid  19225  ablsimpnosubgd  19226  ringidss  19327  ringpropd  19332  imasring  19369  qusring2  19370  kerf1ghm  19497  kerf1hrmOLD  19498  subrg1  19545  subrgmcl  19547  subrgdv  19552  subrgunit  19553  issubdrg  19560  resrhm  19564  lmodprop2d  19696  0lmhm  19812  lmhmpropd  19845  lspfixed  19900  lssacsex  19916  lbsextlem4  19933  quscrng  20013  assapropd  20101  psrelbas  20159  resspsrvsca  20198  subrgpsr  20199  mplcoe1  20246  mplbas2  20251  mplascl  20276  mplmon2cl  20280  mplmon2mul  20281  evlrhm  20309  mpfconst  20314  mhpvscacl  20341  vr1cl2  20361  ply1lss  20364  ply1subrg  20365  psropprmul  20406  evl1vsd  20507  evl1expd  20508  evl1gsumadd  20521  evl1gsummon  20528  znf1o  20698  psgnghm2  20725  elocv  20812  pjff  20856  frlmlss  20895  frlmsubgval  20909  frlmvscafval  20910  frlmvscavalb  20914  frlmvplusgscavalb  20915  frlmphl  20925  uvcresum  20937  frlmssuvc1  20938  frlmssuvc2  20939  frlmsslsp  20940  frlmup1  20942  matring  21052  matassa  21053  mat1  21056  mattposcl  21062  mavmulass  21158  mdetunilem9  21229  matinv  21286  cpmadugsumlemF  21484  cpmadugsumfi  21485  cpmidgsum2  21487  elcls3  21691  mreclatdemoBAD  21704  neiptopnei  21740  resstps  21795  ordtrest2lem  21811  ordtrest2  21812  pnfnei  21828  mnfnei  21829  iscnp2  21847  iscnp4  21871  cnrest2r  21895  lmcls  21910  lmcld  21911  cnt0  21954  cnhaus  21962  isreg2  21985  connclo  22023  1stccnp  22070  loclly  22095  lly1stc  22104  locfincmp  22134  unisngl  22135  comppfsc  22140  kgencmp2  22154  llycmpkgen2  22158  kgen2ss  22163  kgencn3  22166  pttoponconst  22205  txcls  22212  txbasval  22214  dfac14lem  22225  ptcn  22235  ptrescn  22247  txtube  22248  txcmplem1  22249  txlm  22256  txkgen  22260  xkopjcn  22264  cnmptkp  22288  xkoinjcn  22295  qtopkgen  22318  imastps  22329  isr0  22345  r0cld  22346  pt1hmeo  22414  ptuncnv  22415  ptunhmeo  22416  filintn0  22469  trnei  22500  flimfil  22577  flimopn  22583  fbflim2  22585  cnpflf2  22608  flfcnp  22612  flfcnp2  22615  fclsopn  22622  fcfnei  22643  cnpfcf  22649  flfcntr  22651  alexsublem  22652  ptcmplem3  22662  ptcmplem4  22663  cnextfres1  22676  tmdcn2  22697  tmdgsum  22703  tmdgsum2  22704  efmndtmd  22709  symgtgp  22714  tgphaus  22725  tgpt1  22726  qustgplem  22729  prdstmdd  22732  prdstgpd  22733  haustsms  22744  tsmscls  22746  tsmsmhm  22754  tsmsadd  22755  tgptsmscls  22758  tsmssplit  22760  restutop  22846  utopreg  22861  ressusp  22874  ucncn  22894  xmetunirn  22947  ressprdsds  22981  xpsdsval  22991  xblss2ps  23011  blbas  23040  mopntopon  23049  isxms2  23058  imasf1oxms  23099  imasf1oms  23100  prdsxmslem2  23139  tmsxpsval  23148  tngngp2  23261  tngngp  23263  tgioo  23404  metdseq0  23462  cncfmpt2f  23522  cncfcnvcn  23529  cnmptre  23531  cnheibor  23559  nmhmcn  23724  cvsdiv  23736  cvsdivcl  23737  cphsubrglem  23781  cphreccllem  23782  iscmet3  23896  relcmpcmet  23921  bcthlem4  23930  rrxds  23996  rrxvsca  23997  rrxplusgvscavalb  23998  rrxbasefi  24013  rrxmetfi  24015  minveclem4  24035  ivthicc  24059  evthicc  24060  ovolicc2lem4  24121  ovolicc2lem5  24122  iunmbl2  24158  vitalilem3  24211  cncombf  24259  cnmbf  24260  dvres2lem  24508  cpncn  24533  cpnres  24534  dvaddbr  24535  dvmulbr  24536  dvcobr  24543  dvcjbr  24546  dvrec  24552  dvcnvlem  24573  dvlip2  24592  dvivth  24607  lhop2  24612  lhop  24613  dvcnvrelem1  24614  dvcnvrelem2  24615  dvcnvre  24616  ftc1lem6  24638  mdegvscale  24669  mdegvsca  24670  fta1blem  24762  plyaddlem1  24803  plymullem1  24804  coeeulem  24814  tayl0  24950  taylthlem1  24961  taylthlem2  24962  ulmdvlem3  24990  psercnlem2  25012  psercn  25014  efsubm  25135  cxpcn3  25329  loglesqrt  25339  efrlim  25547  ppinprm  25729  chtnprm  25731  dchrptlem1  25840  dchrptlem2  25841  tgbtwnouttr2  26281  tgldim0eq  26289  tgifscgr  26294  iscgrglt  26300  ercgrg  26303  tgcgrxfr  26304  motcgrg  26330  tglngne  26336  tgcolg  26340  tgbtwnconn1lem2  26359  tgbtwnconn1lem3  26360  legtri3  26376  legbtwn  26380  ncolne1  26411  tgisline  26413  tglinethru  26422  coltr3  26434  colline  26435  tglowdim2ln  26437  mirinv  26452  miriso  26456  mirauto  26470  miduniq  26471  krippenlem  26476  midexlem  26478  ragperp  26503  footexALT  26504  footexlem2  26506  perpdragALT  26513  perpdrag  26514  colperpexlem1  26516  colperpexlem3  26518  mideulem2  26520  midex  26523  opphllem1  26533  opphllem3  26535  opphllem4  26536  hlpasch  26542  trgcopy  26590  f1otrg  26657  axlowdimlem16  26743  elntg  26770  eengtrkg  26772  eengtrkge  26773  clwwlkccatlem  27767  grpoidinv2  28292  grpoinv  28302  ubthlem2  28648  shuni  29077  acunirnmpt  30404  acunirnmpt2  30405  acunirnmpt2f  30406  fpwrelmap  30469  fzm1ne1  30512  fzom1ne1  30524  ccatf1  30625  swrdf1  30630  gsummpt2d  30687  odpmco  30730  pmtrcnel  30733  pmtrcnel2  30734  pmtrcnelor  30735  tocyc01  30760  trsp2cyc  30765  cycpmco2f1  30766  cycpmco2rn  30767  cycpmco2lem1  30768  cycpmco2lem2  30769  cycpmco2lem3  30770  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmco2  30775  cycpmconjv  30784  cycpmrn  30785  tocyccntz  30786  rngurd  30857  freshmansdream  30859  qsidomlem1  30965  srasubrg  30989  drgextlsp  30996  matdim  31013  lbslsat  31014  lindsunlem  31020  lbsdiflsp0  31022  dimkerim  31023  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  fldexttr  31048  extdgmul  31051  extdg1id  31053  ordtrest2NEWlem  31165  ordtrest2NEW  31166  lmxrge0  31195  nmmulg  31209  rrhcn  31238  esumadd  31316  esumaddf  31320  esumcocn  31339  measiuns  31476  mbfmco2  31523  dya2iocnrect  31539  omscl  31553  omsf  31554  oms0  31555  sibf0  31592  sibfof  31598  sitgaddlemb  31606  fibp1  31659  ccatmulgnn0dir  31812  cxpcncf1  31866  ftc2re  31869  fsum2dsub  31878  reprf  31883  reprsum  31884  bnj1450  32322  bnj1501  32339  revpfxsfxrev  32362  indispconn  32481  connpconn  32482  pconnpi1  32484  sconnpi1  32486  cvmsss2  32521  cvmliftmolem1  32528  cvmliftlem8  32539  cvmliftlem10  32541  cvmliftlem11  32542  cvmlift2lem9  32558  cvmlift2lem12  32561  cvmlift3lem7  32572  mrsubcv  32757  mrsubff  32759  mrsubccat  32765  elmrsubrn  32767  mrsubco  32768  mrsubvrs  32769  frrlem8  33130  frrlem10  33132  nodenselem5  33192  linethru  33614  ivthALT  33683  neibastop2  33709  filnetlem4  33729  matunitlindflem2  34904  poimirlem1  34908  poimirlem2  34909  poimirlem8  34915  poimirlem9  34916  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimir  34940  broucube  34941  areacirclem4  35000  fdc  35035  isbnd3  35077  prdsbnd  35086  prdstotbnd  35087  prdsbnd2  35088  rrnequiv  35128  reheibor  35132  iscringd  35291  isfldidl  35361  eqvrelth  35861  eqlkr  36250  ldualvsubval  36308  dvalveclem  38176  dia2dimlem5  38219  dia2dimlem9  38223  tendoinvcl  38255  dvhgrp  38258  dvhlveclem  38259  dihpN  38487  dochsnkr2cl  38625  lcfl7lem  38650  lclkr  38684  lclkrs  38690  lcfrvalsnN  38692  lcfrlem4  38696  lcfrlem6  38698  lcfrlem16  38709  lcdvsubval  38769  lcdlkreqN  38773  mapdcl2  38807  mapdincl  38812  mapdlsmcl  38814  mapdpglem3  38826  hdmaprnlem9N  39008  hdmaplkr  39064  hdmapip0  39066  hdmapglem7a  39078  fltnltalem  39323  diophin  39418  acongeq  39629  isnumbasgrplem2  39753  proot1mul  39848  iunrelexpuztr  40113  ntrclsiex  40452  ntrneiiex  40475  ntrneinex  40476  elnelneqd  40604  grurankcld  40618  bccbc  40726  suctrALT  41209  restuni3  41433  disjf1o  41501  disjinfi  41503  choicefi  41512  fsneq  41518  fsneqrn  41523  unirnmapsn  41526  iunmapsn  41529  monoords  41613  elfzolem1  41638  uzfissfz  41643  monoord2xrv  41809  evthiccabs  41820  iooabslt  41823  tgqioo2  41872  islptre  41949  limciccioolb  41951  sumnnodd  41960  limcicciooub  41967  lptre2pt  41970  limcresiooub  41972  limcresioolb  41973  lptioo1cn  41976  reclimc  41983  liminfvalxr  42113  liminfvaluz  42122  limsupvaluz3  42128  fsumcncf  42210  ioccncflimc  42217  cncfuni  42218  icccncfext  42219  cncficcgt0  42220  icocncflimc  42221  cncfdmsn  42222  cncfiooicclem1  42225  cncfiooicc  42226  cncfioobd  42229  cxpcncf2  42232  fprodsub2cncf  42238  fprodadd2cncf  42239  fperdvper  42252  dvcosax  42260  dvnmul  42277  dvnprodlem1  42280  dvnprodlem2  42281  itgsubsticclem  42309  fvvolioof  42323  fvvolicof  42325  stoweidlem26  42360  stoweidlem27  42361  stoweidlem31  42365  stoweidlem34  42368  dirkercncflem2  42438  dirkercncflem3  42439  dirkercncflem4  42440  dirkercncf  42441  fourierdlem16  42457  fourierdlem20  42461  fourierdlem21  42462  fourierdlem22  42463  fourierdlem26  42467  fourierdlem32  42473  fourierdlem33  42474  fourierdlem38  42479  fourierdlem39  42480  fourierdlem46  42486  fourierdlem48  42488  fourierdlem49  42489  fourierdlem53  42493  fourierdlem60  42500  fourierdlem61  42501  fourierdlem69  42509  fourierdlem70  42510  fourierdlem71  42511  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem80  42520  fourierdlem81  42521  fourierdlem82  42522  fourierdlem83  42523  fourierdlem84  42524  fourierdlem85  42525  fourierdlem88  42528  fourierdlem89  42529  fourierdlem91  42531  fourierdlem92  42532  fourierdlem93  42533  fourierdlem100  42540  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem107  42547  fourierdlem111  42551  fourierdlem112  42552  fourierdlem113  42553  fouriersw  42565  fouriercn  42566  etransclem24  42592  etransclem26  42594  etransclem28  42596  etransclem31  42599  etransclem32  42600  etransclem33  42601  etransclem34  42602  etransclem35  42603  etransclem38  42606  rrxtopnfi  42621  rrxtoponfi  42625  qndenserrnbl  42629  qndenserrnopnlem  42631  qndenserrn  42633  rrnprjdstle  42635  ioorrnopnlem  42638  prsal  42652  intsaluni  42661  salgencntex  42675  subsaliuncllem  42689  fge0iccico  42701  sge0sn  42710  sge0tsms  42711  sge0cl  42712  sge0f1o  42713  sge0pr  42725  sge0isum  42758  nnfoctbdjlem  42786  iundjiunlem  42790  iundjiun  42791  meadjiunlem  42796  psmeasure  42802  meaiininclem  42817  caragenelss  42832  omeunile  42836  carageniuncllem1  42852  carageniuncllem2  42853  0ome  42860  isomenndlem  42861  isomennd  42862  hoicvr  42879  ovnpnfelsup  42890  ovncvrrp  42895  ovnsubaddlem1  42901  hoidmv1le  42925  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  hoidmvle  42931  ovnhoilem1  42932  hoi2toco  42938  ovncvr2  42942  hspdifhsp  42947  voncmpl  42952  hoiqssbl  42956  hspmbllem2  42958  hspmbl  42960  hoimbllem  42961  opnvonmbllem2  42964  mblvon  42970  ovolval3  42978  ovolval4lem1  42980  ovnovollem1  42987  ovnovollem2  42988  vonsn  43022  issmflem  43053  sssmf  43064  issmflelem  43070  issmfgtlem  43081  issmfgt  43082  smfaddlem1  43088  issmfgelem  43094  smflimlem3  43098  smfmullem2  43116  smfmullem4  43118  smfsuplem1  43134  smfsupmpt  43138  smfinfmpt  43142  smflimsuplem2  43144  smflimsuplem4  43146  smflimsupmpt  43152  smfliminfmpt  43155  fzoopth  43576  issubmgm2  44106  zlmodzxzel  44452  ply1mulgsum  44493