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

Theorem eleqtrd 2829
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 2813 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 222 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1620  wcel 2127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1842  df-cleq 2741  df-clel 2744
This theorem is referenced by:  eleqtrrd  2830  syl5eleq  2833  syl6eleq  2837  3eltr3d  2841  prel12g  4532  opth1  5080  0nelop  5096  fviss  6406  tfisi  7211  fnwelem  7448  wfrlem17  7588  omeulem1  7819  oeeulem  7838  oeeui  7839  oaabs2  7882  omabs  7884  ercl  7910  erth  7946  ecelqsdm  7972  ordtypelem6  8581  ordtypelem7  8582  cantnfval  8726  cantnfp1lem3  8738  cantnflem4  8750  r1pwss  8808  rankonidlem  8852  rankxplim3  8905  fseqenlem2  9009  iunfictbso  9098  dfac12lem1  9128  dfac12lem2  9129  fin23lem30  9327  iundom2g  9525  fpwwe2lem6  9620  fpwwe2lem9  9623  lincmb01cmp  12479  fzopth  12542  fzoaddel2  12689  fzosubel2  12693  fzocatel  12697  zpnn0elfzo1  12707  fzoend  12724  peano2fzor  12740  monoord2  12997  sermono  12998  expmulnbnd  13161  bcpasc  13273  swrdcl  13589  revcl  13681  revlen  13682  fsum0diag2  14685  isumsplit  14742  fprodser  14849  sadadd  15362  sadass  15366  smuval2  15377  smumul  15388  vdwapun  15851  vdwlem9  15866  ramub1lem1  15903  prdsbasfn  16304  prdsbasprj  16305  pwsplusgval  16323  pwsmulrval  16324  pwsvscafval  16327  xpsaddlem  16408  xpsvsca  16412  xpsle  16414  mreexmrid  16476  homfeqval  16529  comfval2  16535  comfeq  16538  comfeqval  16540  oppccomfpropd  16559  invco  16603  sectepi  16616  issubc3  16681  funcf2  16700  funciso  16706  fthepi  16760  nat1st2nd  16783  fuciso  16807  homarcl2  16857  coapm  16893  setcmon  16909  setcepi  16910  setcsect  16911  setcinv  16912  setciso  16913  catccatid  16924  resscatc  16927  catciso  16929  catcoppccl  16930  catcfuccl  16931  xpccatid  17000  catcxpccl  17019  xpcpropd  17020  evlfcl  17034  curfpropd  17045  hofcl  17071  yonedalem3  17092  yonffthlem  17094  poslubdg  17321  grpidd  17440  gsumress  17448  ismndd  17485  mndpropd  17488  issubmnd  17490  submnd0  17492  imasmnd  17500  frmdelbas  17562  grpidd2  17631  pwsinvg  17700  imasgrp  17703  submmulg  17758  subginvcl  17775  subgcl  17776  subgsub  17778  subgmulg  17780  quseccl  17822  gaid2  17907  submod  18155  odsubdvds  18157  sylow1lem4  18187  sylow2alem2  18204  lsmdisj2  18266  subgdisj1  18275  pj1id  18283  efgsrel  18318  efgrelexlemb  18334  efgcpbl2  18341  frgpcpbl  18343  frgp0  18344  frgpeccl  18345  frgpadd  18347  frgpup3lem  18361  frgpnabllem1  18447  cycsubgcyg  18473  prdsgsum  18548  dprdfeq0  18592  dmdprdsplitlem  18607  dpjidcl  18628  pgpfac1lem3a  18646  pgpfac1lem4  18648  pgpfaclem1  18651  pgpfaclem2  18652  ablfaclem2  18656  ringidss  18748  ringpropd  18753  imasring  18790  qusring2  18791  kerf1hrm  18916  subrg1  18963  subrgmcl  18965  subrgdv  18970  subrgunit  18971  issubdrg  18978  resrhm  18982  lmodprop2d  19098  0lmhm  19213  lmhmpropd  19246  lspfixed  19301  lssacsex  19317  lbsextlem4  19334  quscrng  19413  assapropd  19500  psrelbas  19552  resspsrvsca  19591  subrgpsr  19592  mplcoe1  19638  mplbas2  19643  mplascl  19669  mplmon2cl  19673  mplmon2mul  19674  evlrhm  19698  mpfconst  19703  vr1cl2  19736  ply1lss  19739  ply1subrg  19740  psropprmul  19781  evl1vsd  19881  evl1expd  19882  evl1gsumadd  19895  evl1gsummon  19902  znf1o  20073  psgnghm2  20100  elocv  20185  pjff  20229  frlmlss  20268  frlmsubgval  20281  frlmvscafval  20282  frlmphl  20293  uvcresum  20305  frlmssuvc1  20306  frlmssuvc2  20307  frlmsslsp  20308  frlmup1  20310  matring  20422  matassa  20423  mat1  20426  mattposcl  20432  mavmulass  20528  mdetunilem9  20599  matinv  20656  cpmadugsumlemF  20854  cpmadugsumfi  20855  cpmidgsum2  20857  elcls3  21060  mreclatdemoBAD  21073  neiptopnei  21109  resstps  21164  ordtrest2lem  21180  ordtrest2  21181  pnfnei  21197  mnfnei  21198  iscnp2  21216  iscnp4  21240  cnrest2r  21264  lmcls  21279  lmcld  21280  cnt0  21323  cnhaus  21331  isreg2  21354  connclo  21391  1stccnp  21438  loclly  21463  lly1stc  21472  locfincmp  21502  unisngl  21503  comppfsc  21508  kgencmp2  21522  llycmpkgen2  21526  kgen2ss  21531  kgencn3  21534  pttoponconst  21573  txcls  21580  txbasval  21582  dfac14lem  21593  ptcn  21603  ptrescn  21615  txtube  21616  txcmplem1  21617  txlm  21624  txkgen  21628  xkopjcn  21632  cnmptkp  21656  xkoinjcn  21663  qtopkgen  21686  imastps  21697  isr0  21713  r0cld  21714  pt1hmeo  21782  ptuncnv  21783  ptunhmeo  21784  filintn0  21837  trnei  21868  flimfil  21945  flimopn  21951  fbflim2  21953  cnpflf2  21976  flfcnp  21980  flfcnp2  21983  fclsopn  21990  fcfnei  22011  cnpfcf  22017  flfcntr  22019  alexsublem  22020  ptcmplem3  22030  ptcmplem4  22031  cnextfres1  22044  tmdcn2  22065  tmdgsum  22071  tmdgsum2  22072  symgtgp  22077  tgphaus  22092  tgpt1  22093  qustgplem  22096  prdstmdd  22099  prdstgpd  22100  haustsms  22111  tsmscls  22113  tsmsmhm  22121  tsmsadd  22122  tgptsmscls  22125  tsmssplit  22127  restutop  22213  utopreg  22228  ressusp  22241  ucncn  22261  xmetunirn  22314  ressprdsds  22348  xpsdsval  22358  xblss2ps  22378  blbas  22407  mopntopon  22416  isxms2  22425  imasf1oxms  22466  imasf1oms  22467  prdsxmslem2  22506  tmsxpsval  22515  tngngp2  22628  tngngp  22630  tgioo  22771  metdseq0  22829  cncfmpt2f  22889  cncfcnvcn  22896  cnmptre  22898  cnheibor  22926  nmhmcn  23091  cvsdiv  23103  cvsdivcl  23104  cphsubrglem  23148  cphreccllem  23149  iscmet3  23262  relcmpcmet  23286  bcthlem4  23295  rrxds  23352  minveclem4  23374  ivthicc  23398  evthicc  23399  ovolicc2lem4  23459  ovolicc2lem5  23460  iunmbl2  23496  vitalilem3  23549  cncombf  23595  cnmbf  23596  dvres2lem  23844  cpncn  23869  cpnres  23870  dvaddbr  23871  dvmulbr  23872  dvcobr  23879  dvcjbr  23882  dvrec  23888  dvcnvlem  23909  dvlip2  23928  dvivth  23943  lhop2  23948  lhop  23949  dvcnvrelem1  23950  dvcnvrelem2  23951  dvcnvre  23952  ftc1lem6  23974  mdegvscale  24005  mdegvsca  24006  fta1blem  24098  plyaddlem1  24139  plymullem1  24140  coeeulem  24150  tayl0  24286  taylthlem1  24297  taylthlem2  24298  ulmdvlem3  24326  psercnlem2  24348  psercn  24350  efsubm  24467  cxpcn3  24659  loglesqrt  24669  efrlim  24866  ppinprm  25048  chtnprm  25050  dchrptlem1  25159  dchrptlem2  25160  tgbtwnouttr2  25560  tgldim0eq  25568  tgifscgr  25573  iscgrglt  25579  ercgrg  25582  tgcgrxfr  25583  motcgrg  25609  tglngne  25615  tgcolg  25619  tgbtwnconn1lem2  25638  tgbtwnconn1lem3  25639  legtri3  25655  legbtwn  25659  ncolne1  25690  tgisline  25692  tglinethru  25701  coltr3  25713  colline  25714  tglowdim2ln  25716  mirinv  25731  miriso  25735  mirauto  25749  miduniq  25750  krippenlem  25755  midexlem  25757  ragperp  25782  footex  25783  perpdragALT  25789  perpdrag  25790  colperpexlem1  25792  colperpexlem3  25794  mideulem2  25796  midex  25799  opphllem1  25809  opphllem3  25811  opphllem4  25812  hlpasch  25818  trgcopy  25866  acopyeu  25895  f1otrg  25921  axlowdimlem16  26007  elntg  26034  eengtrkg  26035  eengtrkge  26036  grpoidinv2  27649  grpoinv  27659  ubthlem2  28007  shuni  28439  acunirnmpt  29739  acunirnmpt2  29740  acunirnmpt2f  29741  fpwrelmap  29788  gsummpt2d  30061  rngurd  30068  ordtrest2NEWlem  30248  ordtrest2NEW  30249  lmxrge0  30278  nmmulg  30292  rrhcn  30321  esumadd  30399  esumaddf  30403  esumcocn  30422  measiuns  30560  mbfmco2  30607  dya2iocnrect  30623  omscl  30637  omsf  30638  oms0  30639  sibf0  30676  sibfof  30682  sitgaddlemb  30690  fibp1  30743  ccatmulgnn0dir  30899  cxpcncf1  30953  ftc2re  30956  fsum2dsub  30965  reprf  30970  reprsum  30971  bnj1450  31396  bnj1501  31413  indispconn  31494  connpconn  31495  pconnpi1  31497  sconnpi1  31499  cvmsss2  31534  cvmliftmolem1  31541  cvmliftlem8  31552  cvmliftlem10  31554  cvmliftlem11  31555  cvmlift2lem9  31571  cvmlift2lem12  31574  cvmlift3lem7  31585  mrsubcv  31685  mrsubff  31687  mrsubccat  31693  elmrsubrn  31695  mrsubco  31696  mrsubvrs  31697  nodenselem5  32115  linethru  32537  ivthALT  32607  neibastop2  32633  filnetlem4  32653  matunitlindflem2  33688  poimirlem1  33692  poimirlem2  33693  poimirlem8  33699  poimirlem9  33700  poimirlem16  33707  poimirlem17  33708  poimirlem19  33710  poimirlem20  33711  poimirlem22  33713  poimirlem23  33714  poimir  33724  broucube  33725  areacirclem4  33785  fdc  33823  isbnd3  33865  prdsbnd  33874  prdstotbnd  33875  prdsbnd2  33876  rrnequiv  33916  reheibor  33920  iscringd  34079  isfldidl  34149  eqlkr  34858  ldualvsubval  34916  dvalveclem  36785  dia2dimlem5  36828  dia2dimlem9  36832  tendoinvcl  36864  dvhgrp  36867  dvhlveclem  36868  dihpN  37096  dochsnkr2cl  37234  lcfl7lem  37259  lclkr  37293  lclkrs  37299  lcfrvalsnN  37301  lcfrlem4  37305  lcfrlem6  37307  lcfrlem16  37318  lcdvsubval  37378  lcdlkreqN  37382  mapdcl2  37416  mapdincl  37421  mapdlsmcl  37423  mapdpglem3  37435  hdmaprnlem9N  37620  hdmaplkr  37676  hdmapip0  37678  hdmapglem7a  37690  diophin  37807  acongeq  38021  isnumbasgrplem2  38145  proot1mul  38248  iunrelexpuztr  38482  ntrclsiex  38822  ntrneiiex  38845  ntrneinex  38846  bccbc  39015  suctrALT  39529  restuni3  39769  disjf1o  39846  disjinfi  39848  choicefi  39860  fsneq  39866  fsneqrn  39871  unirnmapsn  39874  iunmapsn  39877  fvelimad  39926  monoords  39979  elfzolem1  40004  uzfissfz  40009  monoord2xrv  40181  evthiccabs  40190  iooabslt  40193  tgqioo2  40246  islptre  40323  limciccioolb  40325  sumnnodd  40334  limcicciooub  40341  lptre2pt  40344  limcresiooub  40346  limcresioolb  40347  lptioo1cn  40350  reclimc  40357  liminfvalxr  40487  liminfvaluz  40496  limsupvaluz3  40502  fsumcncf  40563  ioccncflimc  40570  cncfuni  40571  icccncfext  40572  cncficcgt0  40573  icocncflimc  40574  cncfdmsn  40575  cncfiooicclem1  40578  cncfiooicc  40579  cncfioobd  40582  cxpcncf2  40585  fprodsub2cncf  40591  fprodadd2cncf  40592  fperdvper  40605  dvcosax  40613  dvnmul  40630  dvnprodlem1  40633  dvnprodlem2  40634  itgsubsticclem  40663  fvvolioof  40678  fvvolicof  40680  stoweidlem26  40715  stoweidlem27  40716  stoweidlem31  40720  stoweidlem34  40723  dirkercncflem2  40793  dirkercncflem3  40794  dirkercncflem4  40795  dirkercncf  40796  fourierdlem16  40812  fourierdlem20  40816  fourierdlem21  40817  fourierdlem22  40818  fourierdlem26  40822  fourierdlem32  40828  fourierdlem33  40829  fourierdlem38  40834  fourierdlem39  40835  fourierdlem46  40841  fourierdlem48  40843  fourierdlem49  40844  fourierdlem53  40848  fourierdlem60  40855  fourierdlem61  40856  fourierdlem69  40864  fourierdlem70  40865  fourierdlem71  40866  fourierdlem73  40868  fourierdlem74  40869  fourierdlem75  40870  fourierdlem76  40871  fourierdlem80  40875  fourierdlem81  40876  fourierdlem82  40877  fourierdlem83  40878  fourierdlem84  40879  fourierdlem85  40880  fourierdlem88  40883  fourierdlem89  40884  fourierdlem91  40886  fourierdlem92  40887  fourierdlem93  40888  fourierdlem100  40895  fourierdlem101  40896  fourierdlem103  40898  fourierdlem104  40899  fourierdlem107  40902  fourierdlem111  40906  fourierdlem112  40907  fourierdlem113  40908  fouriersw  40920  fouriercn  40921  etransclem24  40947  etransclem26  40949  etransclem28  40951  etransclem31  40954  etransclem32  40955  etransclem33  40956  etransclem34  40957  etransclem35  40958  etransclem38  40961  rrxbasefi  40975  rrxdsfi  40977  rrxtopnfi  40978  rrxmetfi  40979  rrxtoponfi  40983  qndenserrnbl  40987  qndenserrnopnlem  40989  qndenserrn  40991  rrnprjdstle  40993  ioorrnopnlem  40996  prsal  41010  intsaluni  41019  salgencntex  41033  subsaliuncllem  41047  fge0iccico  41059  sge0sn  41068  sge0tsms  41069  sge0cl  41070  sge0f1o  41071  sge0pr  41083  sge0isum  41116  nnfoctbdjlem  41144  iundjiunlem  41148  iundjiun  41149  meadjiunlem  41154  psmeasure  41160  meaiininclem  41175  caragenelss  41190  omeunile  41194  carageniuncllem1  41210  carageniuncllem2  41211  0ome  41218  isomenndlem  41219  isomennd  41220  hoicvr  41237  ovnpnfelsup  41248  ovncvrrp  41253  ovnsubaddlem1  41259  hoidmv1le  41283  hoidmvlelem2  41285  hoidmvlelem3  41286  hoidmvlelem4  41287  hoidmvle  41289  ovnhoilem1  41290  hoi2toco  41296  ovncvr2  41300  hspdifhsp  41305  voncmpl  41310  hoiqssbl  41314  hspmbllem2  41316  hspmbl  41318  hoimbllem  41319  opnvonmbllem2  41322  mblvon  41328  ovolval3  41336  ovolval4lem1  41338  ovnovollem1  41345  ovnovollem2  41346  vonsn  41380  issmflem  41411  sssmf  41422  issmflelem  41428  issmfgtlem  41439  issmfgt  41440  smfaddlem1  41446  issmfgelem  41452  smflimlem3  41456  smfmullem2  41474  smfmullem4  41476  smfsuplem1  41492  smfsupmpt  41496  smfinfmpt  41500  smflimsuplem2  41502  smflimsuplem4  41504  smflimsupmpt  41510  smfliminfmpt  41513  fzoopth  41816  issubmgm2  42269  zlmodzxzel  42612  ply1mulgsum  42657
  Copyright terms: Public domain W3C validator