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

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
StepHypRef Expression
1 eleqtrd.1 . 2 (𝜑𝐴𝐵)
2 eleqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32eleq2d 2898 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 233 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893
This theorem is referenced by:  eleqtrrd  2916  eleqtrid  2919  eleqtrdi  2923  3eltr3d  2927  prel12g  4788  opth1  5359  0nelop  5378  fvelimad  6726  fviss  6735  tfisi  7561  fnwelem  7816  wfrlem17  7962  omeulem1  8198  oeeulem  8217  oeeui  8218  oaabs2  8262  omabs  8264  ercl  8290  erth  8328  ecelqsdm  8357  ordtypelem6  8976  ordtypelem7  8977  cantnfval  9120  cantnfp1lem3  9132  cantnflem4  9144  r1pwss  9202  rankonidlem  9246  rankxplim3  9299  fseqenlem2  9440  iunfictbso  9529  dfac12lem1  9558  dfac12lem2  9559  fin23lem30  9753  iundom2g  9951  fpwwe2lem6  10046  fpwwe2lem9  10049  lincmb01cmp  12871  fzopth  12934  fzoaddel2  13083  fzosubel2  13087  fzocatel  13091  zpnn0elfzo1  13101  fzoend  13118  peano2fzor  13134  monoord2  13391  sermono  13392  expmulnbnd  13586  bcpasc  13671  hash1elsn  13722  swrdcl  13997  revcl  14113  revlen  14114  fsum0diag2  15128  isumsplit  15185  fprodser  15293  sadadd  15806  sadass  15810  smuval2  15821  smumul  15832  vdwapun  16300  vdwlem9  16315  ramub1lem1  16352  prdsbasfn  16734  prdsbasprj  16735  pwsplusgval  16753  pwsmulrval  16754  pwsvscafval  16757  xpsaddlem  16836  xpsvsca  16840  xpsle  16842  mreexmrid  16904  homfeqval  16957  comfval2  16963  comfeq  16966  comfeqval  16968  oppccomfpropd  16987  invco  17031  sectepi  17044  issubc3  17109  funcf2  17128  fthepi  17188  nat1st2nd  17211  homarcl2  17285  coapm  17321  setcmon  17337  setcepi  17338  setcsect  17339  setcinv  17340  setciso  17341  catccatid  17352  resscatc  17355  catciso  17357  catcoppccl  17358  catcfuccl  17359  xpccatid  17428  catcxpccl  17447  xpcpropd  17448  evlfcl  17462  curfpropd  17473  hofcl  17499  yonedalem3  17520  yonffthlem  17522  poslubdg  17749  grpidd  17871  gsumress  17882  ismndd  17923  mndpropd  17926  issubmnd  17928  submnd0  17930  imasmnd  17939  frmdelbas  18008  grpidd2  18081  pwsinvg  18152  imasgrp  18155  submmulg  18211  subginvcl  18228  subgcl  18229  subgsub  18231  subgmulg  18233  1nsgtrivd  18266  quseccl  18276  gaid2  18373  submod  18625  odsubdvds  18627  sylow1lem4  18657  sylow2alem2  18674  lsmdisj2  18739  subgdisj1  18748  pj1id  18756  efgsrel  18791  efgrelexlemb  18807  efgcpbl2  18814  frgpcpbl  18816  frgp0  18817  frgpeccl  18818  frgpadd  18820  frgpup3lem  18834  frgpnabllem1  18924  cycsubgcyg  18952  prdsgsum  19032  dprdfeq0  19075  dmdprdsplitlem  19090  dpjidcl  19111  pgpfac1lem3a  19129  pgpfac1lem4  19131  pgpfaclem1  19134  pgpfaclem2  19135  ablfaclem2  19139  simpgnsgeqd  19154  simpgnsgbid  19156  ablsimpnosubgd  19157  ringidss  19258  ringpropd  19263  imasring  19300  qusring2  19301  kerf1ghm  19428  kerf1hrmOLD  19429  subrg1  19476  subrgmcl  19478  subrgdv  19483  subrgunit  19484  issubdrg  19491  resrhm  19495  lmodprop2d  19627  0lmhm  19743  lmhmpropd  19776  lspfixed  19831  lssacsex  19847  lbsextlem4  19864  quscrng  19943  assapropd  20031  psrelbas  20089  resspsrvsca  20128  subrgpsr  20129  mplcoe1  20176  mplbas2  20181  mplascl  20206  mplmon2cl  20210  mplmon2mul  20211  evlrhm  20239  mpfconst  20244  mhpvscacl  20271  vr1cl2  20291  ply1lss  20294  ply1subrg  20295  psropprmul  20336  evl1vsd  20437  evl1expd  20438  evl1gsumadd  20451  evl1gsummon  20458  znf1o  20628  psgnghm2  20655  elocv  20742  pjff  20786  frlmlss  20825  frlmsubgval  20839  frlmvscafval  20840  frlmvscavalb  20844  frlmvplusgscavalb  20845  frlmphl  20855  uvcresum  20867  frlmssuvc1  20868  frlmssuvc2  20869  frlmsslsp  20870  frlmup1  20872  matring  20982  matassa  20983  mat1  20986  mattposcl  20992  mavmulass  21088  mdetunilem9  21159  matinv  21216  cpmadugsumlemF  21414  cpmadugsumfi  21415  cpmidgsum2  21417  elcls3  21621  mreclatdemoBAD  21634  neiptopnei  21670  resstps  21725  ordtrest2lem  21741  ordtrest2  21742  pnfnei  21758  mnfnei  21759  iscnp2  21777  iscnp4  21801  cnrest2r  21825  lmcls  21840  lmcld  21841  cnt0  21884  cnhaus  21892  isreg2  21915  connclo  21953  1stccnp  22000  loclly  22025  lly1stc  22034  locfincmp  22064  unisngl  22065  comppfsc  22070  kgencmp2  22084  llycmpkgen2  22088  kgen2ss  22093  kgencn3  22096  pttoponconst  22135  txcls  22142  txbasval  22144  dfac14lem  22155  ptcn  22165  ptrescn  22177  txtube  22178  txcmplem1  22179  txlm  22186  txkgen  22190  xkopjcn  22194  cnmptkp  22218  xkoinjcn  22225  qtopkgen  22248  imastps  22259  isr0  22275  r0cld  22276  pt1hmeo  22344  ptuncnv  22345  ptunhmeo  22346  filintn0  22399  trnei  22430  flimfil  22507  flimopn  22513  fbflim2  22515  cnpflf2  22538  flfcnp  22542  flfcnp2  22545  fclsopn  22552  fcfnei  22573  cnpfcf  22579  flfcntr  22581  alexsublem  22582  ptcmplem3  22592  ptcmplem4  22593  cnextfres1  22606  tmdcn2  22627  tmdgsum  22633  tmdgsum2  22634  symgtgp  22639  tgphaus  22654  tgpt1  22655  qustgplem  22658  prdstmdd  22661  prdstgpd  22662  haustsms  22673  tsmscls  22675  tsmsmhm  22683  tsmsadd  22684  tgptsmscls  22687  tsmssplit  22689  restutop  22775  utopreg  22790  ressusp  22803  ucncn  22823  xmetunirn  22876  ressprdsds  22910  xpsdsval  22920  xblss2ps  22940  blbas  22969  mopntopon  22978  isxms2  22987  imasf1oxms  23028  imasf1oms  23029  prdsxmslem2  23068  tmsxpsval  23077  tngngp2  23190  tngngp  23192  tgioo  23333  metdseq0  23391  cncfmpt2f  23451  cncfcnvcn  23458  cnmptre  23460  cnheibor  23488  nmhmcn  23653  cvsdiv  23665  cvsdivcl  23666  cphsubrglem  23710  cphreccllem  23711  iscmet3  23825  relcmpcmet  23850  bcthlem4  23859  rrxds  23925  rrxvsca  23926  rrxplusgvscavalb  23927  rrxbasefi  23942  rrxmetfi  23944  minveclem4  23964  ivthicc  23988  evthicc  23989  ovolicc2lem4  24050  ovolicc2lem5  24051  iunmbl2  24087  vitalilem3  24140  cncombf  24188  cnmbf  24189  dvres2lem  24437  cpncn  24462  cpnres  24463  dvaddbr  24464  dvmulbr  24465  dvcobr  24472  dvcjbr  24475  dvrec  24481  dvcnvlem  24502  dvlip2  24521  dvivth  24536  lhop2  24541  lhop  24542  dvcnvrelem1  24543  dvcnvrelem2  24544  dvcnvre  24545  ftc1lem6  24567  mdegvscale  24598  mdegvsca  24599  fta1blem  24691  plyaddlem1  24732  plymullem1  24733  coeeulem  24743  tayl0  24879  taylthlem1  24890  taylthlem2  24891  ulmdvlem3  24919  psercnlem2  24941  psercn  24943  efsubm  25062  cxpcn3  25256  loglesqrt  25266  efrlim  25475  ppinprm  25657  chtnprm  25659  dchrptlem1  25768  dchrptlem2  25769  tgbtwnouttr2  26209  tgldim0eq  26217  tgifscgr  26222  iscgrglt  26228  ercgrg  26231  tgcgrxfr  26232  motcgrg  26258  tglngne  26264  tgcolg  26268  tgbtwnconn1lem2  26287  tgbtwnconn1lem3  26288  legtri3  26304  legbtwn  26308  ncolne1  26339  tgisline  26341  tglinethru  26350  coltr3  26362  colline  26363  tglowdim2ln  26365  mirinv  26380  miriso  26384  mirauto  26398  miduniq  26399  krippenlem  26404  midexlem  26406  ragperp  26431  footexALT  26432  footexlem2  26434  perpdragALT  26441  perpdrag  26442  colperpexlem1  26444  colperpexlem3  26446  mideulem2  26448  midex  26451  opphllem1  26461  opphllem3  26463  opphllem4  26464  hlpasch  26470  trgcopy  26518  f1otrg  26585  axlowdimlem16  26671  elntg  26698  eengtrkg  26700  eengtrkge  26701  clwwlkccatlem  27695  grpoidinv2  28220  grpoinv  28230  ubthlem2  28576  shuni  29005  acunirnmpt  30333  acunirnmpt2  30334  acunirnmpt2f  30335  fpwrelmap  30396  fzm1ne1  30439  fzom1ne1  30451  ccatf1  30553  swrdf1  30558  gsummpt2d  30615  odpmco  30658  pmtrcnel  30661  pmtrcnel2  30662  pmtrcnelor  30663  tocyc01  30688  trsp2cyc  30693  cycpmco2f1  30694  cycpmco2rn  30695  cycpmco2lem1  30696  cycpmco2lem2  30697  cycpmco2lem3  30698  cycpmco2lem4  30699  cycpmco2lem5  30700  cycpmco2lem6  30701  cycpmco2lem7  30702  cycpmco2  30703  cycpmconjv  30712  cycpmrn  30713  tocyccntz  30714  rngurd  30785  freshmansdream  30787  qsidomlem1  30883  srasubrg  30889  drgextlsp  30896  matdim  30913  lbslsat  30914  lindsunlem  30920  lbsdiflsp0  30922  dimkerim  30923  fedgmullem1  30925  fedgmullem2  30926  fedgmul  30927  fldexttr  30948  extdgmul  30951  extdg1id  30953  ordtrest2NEWlem  31065  ordtrest2NEW  31066  lmxrge0  31095  nmmulg  31109  rrhcn  31138  esumadd  31216  esumaddf  31220  esumcocn  31239  measiuns  31376  mbfmco2  31423  dya2iocnrect  31439  omscl  31453  omsf  31454  oms0  31455  sibf0  31492  sibfof  31498  sitgaddlemb  31506  fibp1  31559  ccatmulgnn0dir  31712  cxpcncf1  31766  ftc2re  31769  fsum2dsub  31778  reprf  31783  reprsum  31784  bnj1450  32220  bnj1501  32237  revpfxsfxrev  32260  indispconn  32379  connpconn  32380  pconnpi1  32382  sconnpi1  32384  cvmsss2  32419  cvmliftmolem1  32426  cvmliftlem8  32437  cvmliftlem10  32439  cvmliftlem11  32440  cvmlift2lem9  32456  cvmlift2lem12  32459  cvmlift3lem7  32470  mrsubcv  32655  mrsubff  32657  mrsubccat  32663  elmrsubrn  32665  mrsubco  32666  mrsubvrs  32667  frrlem8  33028  frrlem10  33030  nodenselem5  33090  linethru  33512  ivthALT  33581  neibastop2  33607  filnetlem4  33627  matunitlindflem2  34771  poimirlem1  34775  poimirlem2  34776  poimirlem8  34782  poimirlem9  34783  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem22  34796  poimirlem23  34797  poimir  34807  broucube  34808  areacirclem4  34867  fdc  34903  isbnd3  34945  prdsbnd  34954  prdstotbnd  34955  prdsbnd2  34956  rrnequiv  34996  reheibor  35000  iscringd  35159  isfldidl  35229  eqvrelth  35728  eqlkr  36117  ldualvsubval  36175  dvalveclem  38043  dia2dimlem5  38086  dia2dimlem9  38090  tendoinvcl  38122  dvhgrp  38125  dvhlveclem  38126  dihpN  38354  dochsnkr2cl  38492  lcfl7lem  38517  lclkr  38551  lclkrs  38557  lcfrvalsnN  38559  lcfrlem4  38563  lcfrlem6  38565  lcfrlem16  38576  lcdvsubval  38636  lcdlkreqN  38640  mapdcl2  38674  mapdincl  38679  mapdlsmcl  38681  mapdpglem3  38693  hdmaprnlem9N  38875  hdmaplkr  38931  hdmapip0  38933  hdmapglem7a  38945  fltnltalem  39154  diophin  39249  acongeq  39460  isnumbasgrplem2  39584  proot1mul  39679  iunrelexpuztr  39944  ntrclsiex  40283  ntrneiiex  40306  ntrneinex  40307  elnelneqd  40436  grurankcld  40449  bccbc  40557  suctrALT  41040  restuni3  41265  disjf1o  41332  disjinfi  41334  choicefi  41343  fsneq  41349  fsneqrn  41354  unirnmapsn  41357  iunmapsn  41360  monoords  41444  elfzolem1  41469  uzfissfz  41474  monoord2xrv  41640  evthiccabs  41651  iooabslt  41654  tgqioo2  41703  islptre  41780  limciccioolb  41782  sumnnodd  41791  limcicciooub  41798  lptre2pt  41801  limcresiooub  41803  limcresioolb  41804  lptioo1cn  41807  reclimc  41814  liminfvalxr  41944  liminfvaluz  41953  limsupvaluz3  41959  fsumcncf  42041  ioccncflimc  42048  cncfuni  42049  icccncfext  42050  cncficcgt0  42051  icocncflimc  42052  cncfdmsn  42053  cncfiooicclem1  42056  cncfiooicc  42057  cncfioobd  42060  cxpcncf2  42063  fprodsub2cncf  42069  fprodadd2cncf  42070  fperdvper  42083  dvcosax  42091  dvnmul  42108  dvnprodlem1  42111  dvnprodlem2  42112  itgsubsticclem  42140  fvvolioof  42155  fvvolicof  42157  stoweidlem26  42192  stoweidlem27  42193  stoweidlem31  42197  stoweidlem34  42200  dirkercncflem2  42270  dirkercncflem3  42271  dirkercncflem4  42272  dirkercncf  42273  fourierdlem16  42289  fourierdlem20  42293  fourierdlem21  42294  fourierdlem22  42295  fourierdlem26  42299  fourierdlem32  42305  fourierdlem33  42306  fourierdlem38  42311  fourierdlem39  42312  fourierdlem46  42318  fourierdlem48  42320  fourierdlem49  42321  fourierdlem53  42325  fourierdlem60  42332  fourierdlem61  42333  fourierdlem69  42341  fourierdlem70  42342  fourierdlem71  42343  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem76  42348  fourierdlem80  42352  fourierdlem81  42353  fourierdlem82  42354  fourierdlem83  42355  fourierdlem84  42356  fourierdlem85  42357  fourierdlem88  42360  fourierdlem89  42361  fourierdlem91  42363  fourierdlem92  42364  fourierdlem93  42365  fourierdlem100  42372  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  fourierdlem107  42379  fourierdlem111  42383  fourierdlem112  42384  fourierdlem113  42385  fouriersw  42397  fouriercn  42398  etransclem24  42424  etransclem26  42426  etransclem28  42428  etransclem31  42431  etransclem32  42432  etransclem33  42433  etransclem34  42434  etransclem35  42435  etransclem38  42438  rrxtopnfi  42453  rrxtoponfi  42457  qndenserrnbl  42461  qndenserrnopnlem  42463  qndenserrn  42465  rrnprjdstle  42467  ioorrnopnlem  42470  prsal  42484  intsaluni  42493  salgencntex  42507  subsaliuncllem  42521  fge0iccico  42533  sge0sn  42542  sge0tsms  42543  sge0cl  42544  sge0f1o  42545  sge0pr  42557  sge0isum  42590  nnfoctbdjlem  42618  iundjiunlem  42622  iundjiun  42623  meadjiunlem  42628  psmeasure  42634  meaiininclem  42649  caragenelss  42664  omeunile  42668  carageniuncllem1  42684  carageniuncllem2  42685  0ome  42692  isomenndlem  42693  isomennd  42694  hoicvr  42711  ovnpnfelsup  42722  ovncvrrp  42727  ovnsubaddlem1  42733  hoidmv1le  42757  hoidmvlelem2  42759  hoidmvlelem3  42760  hoidmvlelem4  42761  hoidmvle  42763  ovnhoilem1  42764  hoi2toco  42770  ovncvr2  42774  hspdifhsp  42779  voncmpl  42784  hoiqssbl  42788  hspmbllem2  42790  hspmbl  42792  hoimbllem  42793  opnvonmbllem2  42796  mblvon  42802  ovolval3  42810  ovolval4lem1  42812  ovnovollem1  42819  ovnovollem2  42820  vonsn  42854  issmflem  42885  sssmf  42896  issmflelem  42902  issmfgtlem  42913  issmfgt  42914  smfaddlem1  42920  issmfgelem  42926  smflimlem3  42930  smfmullem2  42948  smfmullem4  42950  smfsuplem1  42966  smfsupmpt  42970  smfinfmpt  42974  smflimsuplem2  42976  smflimsuplem4  42978  smflimsupmpt  42984  smfliminfmpt  42987  fzoopth  43408  issubmgm2  43904  efmndtmd  43967  zlmodzxzel  44301  ply1mulgsum  44342
  Copyright terms: Public domain W3C validator