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

Theorem eleqtrd 2547
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 2527 . 2
41, 3mpbid 210 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818
This theorem is referenced by:  eleqtrrd  2548  syl5eleq  2551  syl6eleq  2555  3eltr3d  2559  opth1  4725  0nelop  4742  fviss  5931  tfisi  6693  fnwelem  6915  omeulem1  7250  oeeulem  7269  oeeui  7270  oaabs2  7313  omabs  7315  ercl  7341  erth  7375  ecelqsdm  7400  ordtypelem6  7969  ordtypelem7  7970  cantnfval  8108  cantnfp1lem3  8120  cantnflem4  8132  cantnfvalOLD  8138  cantnfp1lem3OLD  8146  cantnflem4OLD  8154  r1pwss  8223  rankonidlem  8267  rankxplim3  8320  fseqenlem2  8427  iunfictbso  8516  dfac12lem1  8544  dfac12lem2  8545  fin23lem30  8743  iundom2g  8936  fpwwe2lem6  9034  fpwwe2lem9  9037  lincmb01cmp  11692  fzopth  11749  fzoaddel2  11874  fzosubel2  11876  fzocatel  11880  zpnn0elfzo1  11889  fzoend  11903  peano2fzor  11917  monoord2  12138  sermono  12139  expmulnbnd  12298  bcpasc  12399  ccatcl  12593  ccatw2s1p2  12641  swrdcl  12646  revcl  12735  revlen  12736  fsum0diag2  13598  isumsplit  13652  fprodser  13756  sadadd  14117  sadass  14121  smuval2  14132  smumul  14143  vdwapun  14492  vdwlem9  14507  ramub1lem1  14544  prdsbasfn  14868  prdsbasprj  14869  pwsplusgval  14887  pwsmulrval  14888  pwsvscafval  14891  xpsaddlem  14972  xpsvsca  14976  xpsle  14978  mreexmrid  15040  homfeqval  15092  comfval2  15098  comfeq  15101  comfeqval  15103  oppccomfpropd  15122  invco  15165  sectepi  15174  issubc3  15218  funcf2  15237  funciso  15243  fthepi  15297  nat1st2nd  15320  fuciso  15344  homarcl2  15362  coapm  15398  setcmon  15414  setcepi  15415  setcsect  15416  setcinv  15417  setciso  15418  catccatid  15429  resscatc  15432  catciso  15434  catcoppccl  15435  catcfuccl  15436  xpccatid  15457  catcxpccl  15476  xpcpropd  15477  evlfcl  15491  curfpropd  15502  hofcl  15528  yonedalem3  15549  yonffthlem  15551  poslubdg  15779  grpidd  15895  gsumress  15903  ismndd  15943  mndpropd  15946  issubmnd  15948  submnd0  15950  imasmnd  15958  frmdelbas  16021  grpidd2  16087  submmulg  16177  pwsinvg  16182  imasgrp  16186  subginvcl  16210  subgcl  16211  subgsub  16213  subgmulg  16215  quseccl  16257  gaid2  16341  submod  16589  odsubdvds  16591  sylow1lem4  16621  sylow2alem2  16638  lsmdisj2  16700  subgdisj1  16709  pj1id  16717  efgsrel  16752  efgrelexlemb  16768  efgcpbl2  16775  frgpcpbl  16777  frgp0  16778  frgpeccl  16779  frgpadd  16781  frgpup3lem  16795  frgpnabllem1  16877  cycsubgcyg  16903  prdsgsum  17007  prdsgsumOLD  17008  dprdfeq0  17062  dprdfeq0OLD  17069  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  dpjidcl  17107  dpjidclOLD  17114  pgpfac1lem3a  17127  pgpfac1lem4  17129  pgpfaclem1  17132  pgpfaclem2  17133  ablfaclem2  17137  ringidss  17225  ringpropd  17230  imasring  17268  qusring2  17269  kerf1hrm  17392  subrg1  17439  subrgmcl  17441  subrgdv  17446  subrgunit  17447  issubdrg  17454  resrhm  17458  lmodprop2d  17572  0lmhm  17686  lmhmpropd  17719  lspfixed  17774  lssacsex  17790  lbsextlem4  17807  quscrng  17888  assapropd  17976  psrelbas  18032  resspsrvsca  18073  subrgpsr  18074  mplcoe1  18127  mplbas2  18134  mplbas2OLD  18135  mplascl  18161  mplmon2cl  18165  mplmon2mul  18166  evlrhm  18194  mpfconst  18199  vr1cl2  18232  ply1lss  18235  ply1subrg  18236  psropprmul  18279  evl1vsd  18380  evl1expd  18381  evl1gsumadd  18394  evl1gsummon  18401  znf1o  18590  psgnghm2  18617  elocv  18699  pjff  18743  frlmlss  18782  frlmsubgval  18798  frlmvscafval  18799  frlmphl  18812  uvcresum  18824  frlmssuvc1  18825  frlmssuvc2  18826  frlmssuvc1OLD  18827  frlmssuvc2OLD  18828  frlmsslsp  18829  frlmsslspOLD  18830  frlmup1  18832  matring  18945  matassa  18946  mat1  18949  mattposcl  18955  mavmulass  19051  mdetunilem9  19122  matinv  19179  cpmadugsumlemF  19377  cpmadugsumfi  19378  cpmidgsum2  19380  elcls3  19584  mreclatdemoBAD  19597  neiptopnei  19633  resstps  19688  ordtrest2lem  19704  ordtrest2  19705  pnfnei  19721  mnfnei  19722  iscnp2  19740  iscnp4  19764  cnrest2r  19788  lmcls  19803  lmcld  19804  cnt0  19847  cnhaus  19855  isreg2  19878  conclo  19916  1stccnp  19963  loclly  19988  lly1stc  19997  locfincmp  20027  unisngl  20028  comppfsc  20033  kgencmp2  20047  llycmpkgen2  20051  kgen2ss  20056  kgencn3  20059  pttoponconst  20098  txcls  20105  txbasval  20107  dfac14lem  20118  ptcn  20128  ptrescn  20140  txtube  20141  txcmplem1  20142  txlm  20149  txkgen  20153  xkopjcn  20157  cnmptkp  20181  xkoinjcn  20188  qtopkgen  20211  imastps  20222  isr0  20238  r0cld  20239  pt1hmeo  20307  ptuncnv  20308  ptunhmeo  20309  filintn0  20362  trnei  20393  flimfil  20470  flimopn  20476  fbflim2  20478  cnpflf2  20501  flfcnp  20505  flfcnp2  20508  fclsopn  20515  fcfnei  20536  cnpfcf  20542  alexsublem  20544  ptcmplem3  20554  ptcmplem4  20555  cnextfres  20568  tmdcn2  20588  tmdgsum  20594  tmdgsum2  20595  symgtgp  20600  tgphaus  20615  tgpt1  20616  qustgplem  20619  prdstmdd  20622  prdstgpd  20623  haustsms  20634  tsmscls  20636  tsmsmhm  20648  tsmsadd  20649  tgptsmscls  20652  tsmssplit  20654  restutop  20740  utopreg  20755  ressusp  20768  ucncn  20788  xmetunirn  20840  ressprdsds  20874  xpsdsval  20884  xblss2ps  20904  blbas  20933  mopntopon  20942  isxms2  20951  imasf1oxms  20992  imasf1oms  20993  prdsxmslem2  21032  tmsxpsval  21041  tngngp2  21166  tngngp  21168  tgioo  21301  metdseq0  21358  cncfmpt2f  21418  cncfcnvcn  21425  cnmptre  21427  cnheibor  21455  nmhmcn  21603  cvsdiv  21609  cvsdivcl  21610  cphsubrglem  21624  cphreccllem  21625  iscmet3  21732  relcmpcmet  21755  bcthlem4  21766  rrxds  21825  minveclem4  21847  ivthicc  21870  evthicc  21871  ovolicc2lem4  21931  ovolicc2lem5  21932  iunmbl2  21967  vitalilem3  22019  cncombf  22065  cnmbf  22066  dvres2lem  22314  cpncn  22339  cpnres  22340  dvaddbr  22341  dvmulbr  22342  dvcobr  22349  dvcjbr  22352  dvrec  22358  dvcnvlem  22377  dvlip2  22396  dvivth  22411  lhop2  22416  lhop  22417  dvcnvrelem1  22418  dvcnvrelem2  22419  dvcnvre  22420  ftc1lem6  22442  mdegvscale  22475  mdegvsca  22476  fta1blem  22569  plyaddlem1  22610  plymullem1  22611  coeeulem  22621  tayl0  22757  taylthlem1  22768  taylthlem2  22769  ulmdvlem3  22797  psercnlem2  22819  psercn  22821  efsubm  22938  cxpcn3  23122  loglesqrt  23132  efrlim  23299  ppinprm  23426  chtnprm  23428  dchrptlem1  23539  dchrptlem2  23540  tgbtwnouttr2  23886  tgldim0eq  23894  tgifscgr  23900  ercgrg  23908  tgcgrxfr  23909  motcgrg  23931  tglngne  23937  tgcolg  23941  tgbtwnconn1lem2  23960  tgbtwnconn1lem3  23961  legtri3  23977  legbtwn  23981  ncolne1  24005  tgisline  24007  tglinethru  24016  coltr3  24029  colline  24030  tglowdim2ln  24032  mirinv  24047  miriso  24050  mirauto  24061  miduniq  24062  krippenlem  24067  midexlem  24069  ragperp  24094  footex  24095  perpdragALT  24101  perpdrag  24102  colperpexlem1  24104  colperpexlem3  24106  mideulem2  24108  midex  24111  opphllem1  24119  opphllem3  24121  opphllem4  24122  f1otrg  24174  axlowdimlem16  24260  elntg  24287  eengtrkg  24288  eengtrkge  24289  eupap1  24976  grpoidinv2  25220  grpoinv  25229  ubthlem2  25787  shuni  26218  fpwrelmap  27556  rngurd  27778  ordtrest2NEWlem  27904  ordtrest2NEW  27905  lmxrge0  27934  nmmulg  27949  rrhcn  27978  esumadd  28064  esumaddf  28069  esumcocn  28086  measiuns  28188  mbfmco2  28236  dya2iocnrect  28252  oms0  28266  sibf0  28276  sibfof  28282  fibp1  28340  ccatmulgnn0dir  28496  indispcon  28679  conpcon  28680  pconpi1  28682  sconpi1  28684  cvmsss2  28719  cvmliftmolem1  28726  cvmliftlem8  28737  cvmliftlem10  28739  cvmliftlem11  28740  cvmlift2lem9  28756  cvmlift2lem12  28759  cvmlift3lem7  28770  mrsubcv  28870  mrsubff  28872  mrsubccat  28878  elmrsubrn  28880  mrsubco  28881  mrsubvrs  28882  linethru  29803  areacirclem4  30110  ivthALT  30153  neibastop2  30179  filnetlem4  30199  fdc  30238  isbnd3  30280  prdsbnd  30289  prdstotbnd  30290  prdsbnd2  30291  rrnequiv  30331  reheibor  30335  iscringd  30396  isfldidl  30465  diophin  30706  acongeq  30921  isnumbasgrplem2  31053  proot1mul  31156  bccbc  31250  monoords  31496  evthiccabs  31529  iooabslt  31532  islptre  31625  limciccioolb  31627  sumnnodd  31636  limcicciooub  31643  lptre2pt  31646  limcresiooub  31648  limcresioolb  31649  lptioo1cn  31652  reclimc  31659  fsumcncf  31680  ioccncflimc  31688  cncfuni  31689  icccncfext  31690  cncficcgt0  31691  icocncflimc  31692  cncfdmsn  31693  cncfiooicclem1  31696  cncfiooicc  31697  cncfioobd  31700  cxpcncf2  31703  fperdvper  31715  dvcosax  31723  dvnmul  31740  dvnprodlem1  31743  dvnprodlem2  31744  itgsubsticclem  31774  stoweidlem26  31808  stoweidlem27  31809  stoweidlem31  31813  stoweidlem34  31816  dirkercncflem2  31886  dirkercncflem3  31887  dirkercncflem4  31888  dirkercncf  31889  fourierdlem16  31905  fourierdlem20  31909  fourierdlem21  31910  fourierdlem22  31911  fourierdlem26  31915  fourierdlem32  31921  fourierdlem33  31922  fourierdlem38  31927  fourierdlem39  31928  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem53  31942  fourierdlem60  31949  fourierdlem61  31950  fourierdlem69  31958  fourierdlem70  31959  fourierdlem71  31960  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem80  31969  fourierdlem81  31970  fourierdlem82  31971  fourierdlem83  31972  fourierdlem84  31973  fourierdlem85  31974  fourierdlem88  31977  fourierdlem89  31978  fourierdlem91  31980  fourierdlem92  31981  fourierdlem93  31982  fourierdlem100  31989  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem107  31996  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  fouriersw  32014  fouriercn  32015  etransclem24  32041  etransclem26  32043  etransclem28  32045  etransclem31  32048  etransclem32  32049  etransclem33  32050  etransclem34  32051  etransclem35  32052  etransclem38  32055  el2fzo  32339  fzoopth  32340  issubmgm2  32478  zlmodzxzel  32944  ply1mulgsum  32990  suctrALT  33626  bnj1450  34106  bnj1501  34123  eqlkr  34824  ldualvsubval  34882  dvalveclem  36752  dia2dimlem5  36795  dia2dimlem9  36799  tendoinvcl  36831  dvhgrp  36834  dvhlveclem  36835  dihpN  37063  dochsnkr2cl  37201  lcfl7lem  37226  lclkr  37260  lclkrs  37266  lcfrvalsnN  37268  lcfrlem4  37272  lcfrlem6  37274  lcfrlem16  37285  lcdvsubval  37345  lcdlkreqN  37349  mapdcl2  37383  mapdincl  37388  mapdlsmcl  37390  mapdpglem3  37402  hdmaprnlem9N  37587  hdmaplkr  37643  hdmapip0  37645  hdmapglem7a  37657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator