MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleqtrd Structured version   Visualization version   GIF version

Theorem eleqtrd 2689
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
StepHypRef Expression
1 eleqtrd.1 . 2 (𝜑𝐴𝐵)
2 eleqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32eleq2d 2672 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 220 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2602  df-clel 2605
This theorem is referenced by:  eleqtrrd  2690  syl5eleq  2693  syl6eleq  2697  3eltr3d  2701  opth1  4864  0nelop  4880  fviss  6151  tfisi  6928  fnwelem  7157  wfrlem17  7296  omeulem1  7527  oeeulem  7546  oeeui  7547  oaabs2  7590  omabs  7592  ercl  7618  erth  7656  ecelqsdm  7682  ordtypelem6  8289  ordtypelem7  8290  cantnfval  8426  cantnfp1lem3  8438  cantnflem4  8450  r1pwss  8508  rankonidlem  8552  rankxplim3  8605  fseqenlem2  8709  iunfictbso  8798  dfac12lem1  8826  dfac12lem2  8827  fin23lem30  9025  iundom2g  9219  fpwwe2lem6  9314  fpwwe2lem9  9317  lincmb01cmp  12145  fzopth  12207  fzoaddel2  12349  fzosubel2  12353  fzocatel  12357  zpnn0elfzo1  12366  fzoend  12383  peano2fzor  12399  monoord2  12652  sermono  12653  expmulnbnd  12816  bcpasc  12928  swrdcl  13220  revcl  13310  revlen  13311  fsum0diag2  14306  isumsplit  14360  fprodser  14467  sadadd  14976  sadass  14980  smuval2  14991  smumul  15002  vdwapun  15465  vdwlem9  15480  ramub1lem1  15517  prdsbasfn  15903  prdsbasprj  15904  pwsplusgval  15922  pwsmulrval  15923  pwsvscafval  15926  xpsaddlem  16007  xpsvsca  16011  xpsle  16013  mreexmrid  16075  homfeqval  16129  comfval2  16135  comfeq  16138  comfeqval  16140  oppccomfpropd  16159  invco  16203  sectepi  16216  issubc3  16281  funcf2  16300  funciso  16306  fthepi  16360  nat1st2nd  16383  fuciso  16407  homarcl2  16457  coapm  16493  setcmon  16509  setcepi  16510  setcsect  16511  setcinv  16512  setciso  16513  catccatid  16524  resscatc  16527  catciso  16529  catcoppccl  16530  catcfuccl  16531  xpccatid  16600  catcxpccl  16619  xpcpropd  16620  evlfcl  16634  curfpropd  16645  hofcl  16671  yonedalem3  16692  yonffthlem  16694  poslubdg  16921  grpidd  17040  gsumress  17048  ismndd  17085  mndpropd  17088  issubmnd  17090  submnd0  17092  imasmnd  17100  frmdelbas  17162  grpidd2  17231  pwsinvg  17300  imasgrp  17303  submmulg  17358  subginvcl  17375  subgcl  17376  subgsub  17378  subgmulg  17380  quseccl  17422  gaid2  17508  submod  17756  odsubdvds  17758  sylow1lem4  17788  sylow2alem2  17805  lsmdisj2  17867  subgdisj1  17876  pj1id  17884  efgsrel  17919  efgrelexlemb  17935  efgcpbl2  17942  frgpcpbl  17944  frgp0  17945  frgpeccl  17946  frgpadd  17948  frgpup3lem  17962  frgpnabllem1  18048  cycsubgcyg  18074  prdsgsum  18149  dprdfeq0  18193  dmdprdsplitlem  18208  dpjidcl  18229  pgpfac1lem3a  18247  pgpfac1lem4  18249  pgpfaclem1  18252  pgpfaclem2  18253  ablfaclem2  18257  ringidss  18349  ringpropd  18354  imasring  18391  qusring2  18392  kerf1hrm  18515  subrg1  18562  subrgmcl  18564  subrgdv  18569  subrgunit  18570  issubdrg  18577  resrhm  18581  lmodprop2d  18697  0lmhm  18810  lmhmpropd  18843  lspfixed  18898  lssacsex  18914  lbsextlem4  18931  quscrng  19010  assapropd  19097  psrelbas  19149  resspsrvsca  19188  subrgpsr  19189  mplcoe1  19235  mplbas2  19240  mplascl  19266  mplmon2cl  19270  mplmon2mul  19271  evlrhm  19295  mpfconst  19300  vr1cl2  19333  ply1lss  19336  ply1subrg  19337  psropprmul  19378  evl1vsd  19478  evl1expd  19479  evl1gsumadd  19492  evl1gsummon  19499  znf1o  19667  psgnghm2  19694  elocv  19779  pjff  19823  frlmlss  19862  frlmsubgval  19875  frlmvscafval  19876  frlmphl  19887  uvcresum  19899  frlmssuvc1  19900  frlmssuvc2  19901  frlmsslsp  19902  frlmup1  19904  matring  20016  matassa  20017  mat1  20020  mattposcl  20026  mavmulass  20122  mdetunilem9  20193  matinv  20250  cpmadugsumlemF  20448  cpmadugsumfi  20449  cpmidgsum2  20451  elcls3  20645  mreclatdemoBAD  20658  neiptopnei  20694  resstps  20749  ordtrest2lem  20765  ordtrest2  20766  pnfnei  20782  mnfnei  20783  iscnp2  20801  iscnp4  20825  cnrest2r  20849  lmcls  20864  lmcld  20865  cnt0  20908  cnhaus  20916  isreg2  20939  conclo  20976  1stccnp  21023  loclly  21048  lly1stc  21057  locfincmp  21087  unisngl  21088  comppfsc  21093  kgencmp2  21107  llycmpkgen2  21111  kgen2ss  21116  kgencn3  21119  pttoponconst  21158  txcls  21165  txbasval  21167  dfac14lem  21178  ptcn  21188  ptrescn  21200  txtube  21201  txcmplem1  21202  txlm  21209  txkgen  21213  xkopjcn  21217  cnmptkp  21241  xkoinjcn  21248  qtopkgen  21271  imastps  21282  isr0  21298  r0cld  21299  pt1hmeo  21367  ptuncnv  21368  ptunhmeo  21369  filintn0  21423  trnei  21454  flimfil  21531  flimopn  21537  fbflim2  21539  cnpflf2  21562  flfcnp  21566  flfcnp2  21569  fclsopn  21576  fcfnei  21597  cnpfcf  21603  flfcntr  21605  alexsublem  21606  ptcmplem3  21616  ptcmplem4  21617  cnextfres1  21630  tmdcn2  21651  tmdgsum  21657  tmdgsum2  21658  symgtgp  21663  tgphaus  21678  tgpt1  21679  qustgplem  21682  prdstmdd  21685  prdstgpd  21686  haustsms  21697  tsmscls  21699  tsmsmhm  21707  tsmsadd  21708  tgptsmscls  21711  tsmssplit  21713  restutop  21799  utopreg  21814  ressusp  21827  ucncn  21847  xmetunirn  21900  ressprdsds  21934  xpsdsval  21944  xblss2ps  21964  blbas  21993  mopntopon  22002  isxms2  22011  imasf1oxms  22052  imasf1oms  22053  prdsxmslem2  22092  tmsxpsval  22101  tngngp2  22214  tngngp  22216  tgioo  22355  metdseq0  22413  cncfmpt2f  22473  cncfcnvcn  22480  cnmptre  22482  cnheibor  22510  nmhmcn  22676  cvsdiv  22688  cvsdivcl  22689  cphsubrglem  22730  cphreccllem  22731  iscmet3  22844  relcmpcmet  22868  bcthlem4  22877  rrxds  22934  minveclem4  22956  ivthicc  22979  evthicc  22980  ovolicc2lem4  23040  ovolicc2lem5  23041  iunmbl2  23077  vitalilem3  23130  cncombf  23176  cnmbf  23177  dvres2lem  23425  cpncn  23450  cpnres  23451  dvaddbr  23452  dvmulbr  23453  dvcobr  23460  dvcjbr  23463  dvrec  23469  dvcnvlem  23488  dvlip2  23507  dvivth  23522  lhop2  23527  lhop  23528  dvcnvrelem1  23529  dvcnvrelem2  23530  dvcnvre  23531  ftc1lem6  23553  mdegvscale  23584  mdegvsca  23585  fta1blem  23677  plyaddlem1  23718  plymullem1  23719  coeeulem  23729  tayl0  23865  taylthlem1  23876  taylthlem2  23877  ulmdvlem3  23905  psercnlem2  23927  psercn  23929  efsubm  24046  cxpcn3  24234  loglesqrt  24244  efrlim  24441  ppinprm  24623  chtnprm  24625  dchrptlem1  24734  dchrptlem2  24735  tgbtwnouttr2  25135  tgldim0eq  25143  tgifscgr  25149  iscgrglt  25155  ercgrg  25158  tgcgrxfr  25159  motcgrg  25185  tglngne  25191  tgcolg  25195  tgbtwnconn1lem2  25214  tgbtwnconn1lem3  25215  legtri3  25231  legbtwn  25235  ncolne1  25266  tgisline  25268  tglinethru  25277  coltr3  25289  colline  25290  tglowdim2ln  25292  mirinv  25307  miriso  25311  mirauto  25325  miduniq  25326  krippenlem  25331  midexlem  25333  ragperp  25358  footex  25359  perpdragALT  25365  perpdrag  25366  colperpexlem1  25368  colperpexlem3  25370  mideulem2  25372  midex  25375  opphllem1  25385  opphllem3  25387  opphllem4  25388  hlpasch  25394  trgcopy  25442  acopyeu  25471  f1otrg  25497  axlowdimlem16  25583  elntg  25610  eengtrkg  25611  eengtrkge  25612  eupap1  26297  grpoidinv2  26547  grpoinv  26557  ubthlem2  26945  shuni  27377  acunirnmpt  28675  acunirnmpt2  28676  acunirnmpt2f  28677  fpwrelmap  28730  gsummpt2d  28946  rngurd  28953  ordtrest2NEWlem  29130  ordtrest2NEW  29131  lmxrge0  29160  nmmulg  29174  rrhcn  29203  esumadd  29280  esumaddf  29284  esumcocn  29303  measiuns  29441  mbfmco2  29488  dya2iocnrect  29504  omscl  29518  omsf  29519  oms0  29520  sibf0  29557  sibfof  29563  sitgaddlemb  29571  fibp1  29624  ccatmulgnn0dir  29779  bnj1450  30206  bnj1501  30223  indispcon  30304  conpcon  30305  pconpi1  30307  sconpi1  30309  cvmsss2  30344  cvmliftmolem1  30351  cvmliftlem8  30362  cvmliftlem10  30364  cvmliftlem11  30365  cvmlift2lem9  30381  cvmlift2lem12  30384  cvmlift3lem7  30395  mrsubcv  30495  mrsubff  30497  mrsubccat  30503  elmrsubrn  30505  mrsubco  30506  mrsubvrs  30507  linethru  31264  ivthALT  31334  neibastop2  31360  filnetlem4  31380  matunitlindflem2  32400  poimirlem1  32404  poimirlem2  32405  poimirlem8  32411  poimirlem9  32412  poimirlem16  32419  poimirlem17  32420  poimirlem19  32422  poimirlem20  32423  poimirlem22  32425  poimirlem23  32426  poimir  32436  broucube  32437  areacirclem4  32497  fdc  32535  isbnd3  32577  prdsbnd  32586  prdstotbnd  32587  prdsbnd2  32588  rrnequiv  32628  reheibor  32632  iscringd  32791  isfldidl  32861  eqlkr  33228  ldualvsubval  33286  dvalveclem  35156  dia2dimlem5  35199  dia2dimlem9  35203  tendoinvcl  35235  dvhgrp  35238  dvhlveclem  35239  dihpN  35467  dochsnkr2cl  35605  lcfl7lem  35630  lclkr  35664  lclkrs  35670  lcfrvalsnN  35672  lcfrlem4  35676  lcfrlem6  35678  lcfrlem16  35689  lcdvsubval  35749  lcdlkreqN  35753  mapdcl2  35787  mapdincl  35792  mapdlsmcl  35794  mapdpglem3  35806  hdmaprnlem9N  35991  hdmaplkr  36047  hdmapip0  36049  hdmapglem7a  36061  diophin  36178  acongeq  36392  isnumbasgrplem2  36517  proot1mul  36620  iunrelexpuztr  36854  ntrclsiex  37195  ntrneiiex  37218  ntrneinex  37219  bccbc  37390  suctrALT  37907  restuni3  38157  disjf1o  38197  disjinfi  38199  choicefi  38211  fsneq  38217  fsneqrn  38222  unirnmapsn  38225  iunmapsn  38228  monoords  38276  elfzolem1  38302  uzfissfz  38307  evthiccabs  38389  iooabslt  38392  tgqioo2  38445  islptre  38510  limciccioolb  38512  sumnnodd  38521  limcicciooub  38528  lptre2pt  38531  limcresiooub  38533  limcresioolb  38534  lptioo1cn  38537  reclimc  38544  fsumcncf  38587  ioccncflimc  38595  cncfuni  38596  icccncfext  38597  cncficcgt0  38598  icocncflimc  38599  cncfdmsn  38600  cncfiooicclem1  38603  cncfiooicc  38604  cncfioobd  38607  cxpcncf2  38610  fprodsub2cncf  38616  fprodadd2cncf  38617  fperdvper  38632  dvcosax  38640  dvnmul  38657  dvnprodlem1  38660  dvnprodlem2  38661  itgsubsticclem  38691  fvvolioof  38706  fvvolicof  38708  stoweidlem26  38743  stoweidlem27  38744  stoweidlem31  38748  stoweidlem34  38751  dirkercncflem2  38821  dirkercncflem3  38822  dirkercncflem4  38823  dirkercncf  38824  fourierdlem16  38840  fourierdlem20  38844  fourierdlem21  38845  fourierdlem22  38846  fourierdlem26  38850  fourierdlem32  38856  fourierdlem33  38857  fourierdlem38  38862  fourierdlem39  38863  fourierdlem46  38869  fourierdlem48  38871  fourierdlem49  38872  fourierdlem53  38876  fourierdlem60  38883  fourierdlem61  38884  fourierdlem69  38892  fourierdlem70  38893  fourierdlem71  38894  fourierdlem73  38896  fourierdlem74  38897  fourierdlem75  38898  fourierdlem76  38899  fourierdlem80  38903  fourierdlem81  38904  fourierdlem82  38905  fourierdlem83  38906  fourierdlem84  38907  fourierdlem85  38908  fourierdlem88  38911  fourierdlem89  38912  fourierdlem91  38914  fourierdlem92  38915  fourierdlem93  38916  fourierdlem100  38923  fourierdlem101  38924  fourierdlem103  38926  fourierdlem104  38927  fourierdlem107  38930  fourierdlem111  38934  fourierdlem112  38935  fourierdlem113  38936  fouriersw  38948  fouriercn  38949  etransclem24  38975  etransclem26  38977  etransclem28  38979  etransclem31  38982  etransclem32  38983  etransclem33  38984  etransclem34  38985  etransclem35  38986  etransclem38  38989  rrxbasefi  39003  rrxdsfi  39005  rrxtopnfi  39006  rrxmetfi  39007  rrxtoponfi  39011  qndenserrnbl  39015  qndenserrnopnlem  39017  qndenserrn  39019  rrnprjdstle  39021  ioorrnopnlem  39024  prsal  39038  intsaluni  39047  salgencntex  39061  subsaliuncllem  39075  fge0iccico  39087  sge0sn  39096  sge0tsms  39097  sge0cl  39098  sge0f1o  39099  sge0pr  39111  sge0isum  39144  nnfoctbdjlem  39172  iundjiunlem  39176  iundjiun  39177  meadjiunlem  39182  psmeasure  39188  meaiininclem  39200  caragenelss  39215  omeunile  39219  carageniuncllem1  39235  carageniuncllem2  39236  0ome  39243  isomenndlem  39244  isomennd  39245  hoicvr  39262  ovnpnfelsup  39273  ovncvrrp  39278  ovnsubaddlem1  39284  hoidmv1le  39308  hoidmvlelem2  39310  hoidmvlelem3  39311  hoidmvlelem4  39312  hoidmvle  39314  ovnhoilem1  39315  hoi2toco  39321  ovncvr2  39325  hspdifhsp  39330  voncmpl  39335  hoiqssbl  39339  hspmbllem2  39341  hspmbl  39343  hoimbllem  39344  opnvonmbllem2  39347  mblvon  39353  ovolval3  39361  ovolval4lem1  39363  ovnovollem1  39370  ovnovollem2  39371  vonval2  39383  vonsn  39406  issmflem  39437  sssmf  39449  issmflelem  39455  issmfgtlem  39466  issmfgt  39467  smfaddlem1  39473  issmfgelem  39479  smflimlem3  39483  smfmullem2  39501  smfmullem4  39503  fzoopth  40207  issubmgm2  41602  zlmodzxzel  41948  ply1mulgsum  41994
  Copyright terms: Public domain W3C validator