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

Theorem eleqtrrd 2548
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eleqtrrd.1
eleqtrrd.2
Assertion
Ref Expression
eleqtrrd

Proof of Theorem eleqtrrd
StepHypRef Expression
1 eleqtrrd.1 . 2
2 eleqtrrd.2 . . 3
32eqcomd 2465 . 2
41, 3eleqtrd 2547 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818
This theorem is referenced by:  3eltr4d  2560  disjxiun  4449  eldmressnsn  5318  elimdelov  6378  elovmpt3rab1  6536  fnwelem  6915  tfrlem13  7078  tz7.44-2  7092  omordi  7234  oneo  7249  omeulem2  7251  oeordi  7255  oeeui  7270  nnneo  7319  erref  7350  en1uniel  7607  omxpenlem  7638  unblem3  7794  dffi3  7911  ordtypelem10  7973  oismo  7986  cantnff  8114  cantnfp1lem3  8120  cantnflem1  8129  cantnfp1lem3OLD  8146  cantnflem1OLD  8152  cnfcom  8165  cnfcomOLD  8173  r1ordg  8217  r1pwss  8223  rankwflemb  8232  r1elwf  8235  rankidb  8239  rankonidlem  8267  fseqenlem2  8427  dfac12lem1  8544  dfac12lem2  8545  pwsdompw  8605  ackbij2lem3  8642  ackbij2  8644  cfsmolem  8671  isfin4-3  8716  hsmexlem4  8830  ttukeylem3  8912  ttukeylem7  8916  iundom2g  8936  fpwwe2lem9  9037  canthwelem  9049  pwfseqlem4  9061  winalim2  9095  r1wunlim  9136  tskmid  9239  fzopth  11749  fzoss2  11853  fzosubel3  11877  elfzomin  11887  elfzonlteqm1  11891  fzoend  11903  fzofzp1  11909  fzofzp1b  11910  peano2fzor  11917  zmodfzo  12018  seqf1olem2  12147  bcn2  12397  ccatval3  12597  ccatw2s1p1  12640  ccatw2s1p2  12641  ccat2s1fvw  12642  swrdccat2  12683  swrdswrd  12685  wrdeqcats1  12699  swrdccatin12  12716  splfv1  12731  revcl  12735  revlen  12736  revccat  12740  revrev  12741  cshwidxmod  12774  revco  12800  limsupgre  13304  summolem2a  13537  fsumm1  13566  fsumcom2  13589  prodmolem2a  13741  fprodm1  13771  fprodcom2  13788  prmreclem4  14437  prmreclem5  14438  vdwapid1  14493  vdwlem5  14503  vdwlem8  14506  vdwnnlem2  14514  ramub1lem1  14544  ramub1lem2  14545  mrieqvlemd  15026  mreexd  15039  mreexexlemd  15041  catcocl  15082  catass  15083  moni  15131  epii  15138  inviso1  15160  episect  15175  catsubcat  15208  subccocl  15214  fullsubc  15219  funcco  15240  resf2nd  15264  funcres  15265  fthepi  15297  nati  15324  arwhoma  15372  catccatid  15429  resscatc  15432  catcisolem  15433  catcoppccl  15435  catcfuccl  15436  xpcco  15452  xpcco2  15456  xpccatid  15457  prfcl  15472  catcxpccl  15476  curf12  15496  curf1cl  15497  curf2  15498  curf2cl  15500  curfcl  15501  uncf2  15506  uncfcurf  15508  diag12  15513  diag2  15514  curf2ndf  15516  hofcl  15528  oppchofcl  15529  oyoncl  15539  yonedalem3a  15543  yonedalem4b  15545  yonedalem22  15547  yonedalem3b  15548  yonedalem3  15549  yonedainv  15550  yonffthlem  15551  latcl2  15678  latlem  15679  latjcom  15689  latmcom  15705  clatlem  15741  clatlubcl2  15743  clatglbcl2  15745  acsfiindd  15807  gsumpropd2lem  15900  mndpropd  15946  imasmnd  15958  frmdmnd  16027  frmdgsum  16030  grpsubpropd2  16141  imasgrp  16186  subg0  16207  0ghm  16281  resghm2  16284  ghmco  16286  pwsdiagghm  16294  psgnunilem1  16518  psgnunilem5  16519  psgnunilem2  16520  psgnunilem3  16521  sylow1lem4  16621  sylow1lem5  16622  efglem  16734  efgtf  16740  efginvrel2  16745  efginvrel1  16746  efgsdmi  16750  efgs1b  16754  efgsres  16756  efgsfo  16757  efgredleme  16761  efgredlemc  16763  efgredlem  16765  efgcpbllemb  16773  frgp0  16778  frgpadd  16781  frgpinv  16782  vrgpf  16786  vrgpinv  16787  frgpuplem  16790  frgpup1  16793  frgpup2  16794  frgpup3lem  16795  frgpnabllem1  16877  frgpnabllem2  16878  gsumval3OLD  16908  gsumval3  16911  dprdfid  17057  dprdfidOLD  17064  dprdsn  17083  dprd2da  17091  dpjidcl  17107  dpjidclOLD  17114  pgpfac1lem2  17126  pgpfaclem3  17134  ringpropd  17230  imasring  17268  qusring2  17269  pwsco1rhm  17387  pwsco2rhm  17388  subrgunit  17447  pwsdiagrhm  17462  isabvd  17469  lmodprop2d  17572  islssd  17582  prdsvscacl  17614  prdslmodd  17615  islmhm2  17684  lmhmco  17689  lmhmplusg  17690  lmhmvsca  17691  lmhmpropd  17719  lsppreli  17736  lspsnel4  17770  lssacsex  17790  lspsnat  17791  qus1  17883  qusrhm  17885  assapropd  17976  psr0cl  18047  psrnegcl  18049  psr1cl  18055  resspsrmul  18072  subrgpsr  18074  mvrf  18080  mplmon  18125  mplcoe1  18127  subrgasclcl  18164  mplind  18167  evlslem1  18184  subrgply1  18274  psrplusgpropd  18277  ply1coe  18337  cply1coe0bi  18342  lply1binomsc  18349  evls1val  18357  evls1rhm  18359  evl1val  18365  evl1rhm  18368  pf1ind  18391  evl1scvarpw  18399  znf1o  18590  cssmre  18724  dsmmlss  18775  frlmsplit2  18803  frlmbas3  18807  frlmup1  18832  matbas2i  18924  matplusg2  18929  matvsca2  18930  matsubgcell  18936  matvscacell  18938  mpt2matmul  18948  mavmulval  19047  mavmulcl  19049  mavmulass  19051  mavmul0  19054  mavmumamul1  19057  m1detdiag  19099  cramerimplem2  19186  mat2pmatmul  19232  mat2pmatlin  19236  monmatcollpw  19280  pmatcollpwfi  19283  mply1topmatcl  19306  pm2mpghm  19317  pm2mpmhmlem2  19320  pm2mp  19326  chpmat1dlem  19336  chpmat1d  19337  chpdmatlem0  19338  chpscmat  19343  chpscmatgsumbin  19345  chpscmatgsummon  19346  chfacfscmulcl  19358  cpmadugsumlemB  19375  cpmadugsumlemC  19376  chcoeffeqlem  19386  cldmreon  19595  neiptopreu  19634  maxlp  19648  ordttopon  19694  ordtrest2lem  19704  cnprcl2  19752  lmcnp  19805  resthauslem  19864  hauscmplem  19906  1stcfb  19946  2ndcctbss  19956  2ndcomap  19959  dis2ndc  19961  loclly  19988  hausllycmp  19995  locfincmp  20027  dissnref  20029  kgeni  20038  kgenidm  20048  ptpjpre2  20081  xkoopn  20090  txopn  20103  ptpjopn  20113  ptcldmpt  20115  ptcls  20117  pthaus  20139  txkgen  20153  xkohaus  20154  xkopt  20156  txcon  20190  imastps  20222  kqid  20229  kqopn  20235  kqcld  20236  isr0  20238  indishmph  20299  pt1hmeo  20307  ptuncnv  20308  ptunhmeo  20309  t0kq  20319  filcon  20384  uzrest  20398  uffixsn  20426  fmfnfmlem2  20456  flimss2  20473  flimss1  20474  flimclslem  20485  flfcnp  20505  fclsfnflim  20528  uffclsflim  20532  fcfelbas  20537  alexsublem  20544  alexsub  20545  cnextcn  20567  cnextfres  20568  tmdgsum  20594  distgp  20598  indistgp  20599  symgtgp  20600  ghmcnp  20613  qustgpopn  20618  qustgplem  20619  qustgphaus  20621  prdstmdd  20622  prdstgpd  20623  tsmsid  20638  tsmsidOLD  20641  tsmssubm  20644  tsmsmhm  20648  tsmsadd  20649  tsmssplit  20654  utop2nei  20753  utop3cls  20754  neipcfilu  20799  cnextucn  20806  ucnextcn  20807  blpnfctr  20939  lpbl  21006  met2ndci  21025  tmsxps  21039  metcnpi  21047  metcnpi2  21048  metcnpi3  21049  metustidOLD  21062  metustid  21063  metustsymOLD  21064  metustsym  21065  metustexhalfOLD  21066  metustexhalf  21067  subgngp  21149  ngptgp  21150  sranlm  21193  nlmvscn  21196  nrginvrcn  21200  lssnlm  21209  nghmcn  21252  iccntr  21326  icccmplem2  21328  msdcn  21346  cncfmptc  21415  cncfmptid  21416  cncfmpt2f  21418  icoopnst  21439  iocopnst  21440  nmoleub2lem3  21598  nmoleub3  21602  nmhmcn  21603  ipcn  21686  cfilfcls  21713  caucfil  21722  equivcau  21739  caubl  21746  flimcfil  21752  rrxdstprj1  21836  minveclem3b  21843  minveclem4  21847  ovolicc2lem3  21930  ovolicc2lem4  21931  opnmbllem  22010  vitalilem2  22018  mbfsup  22071  mbfinf  22072  mbfi1fseqlem4  22125  limccnp  22295  limccnp2  22296  dvreslem  22313  dvres2lem  22314  dvidlem  22319  dvcnp2  22323  dvcn  22324  dvaddbr  22341  dvmulbr  22342  dvcmul  22347  dvcof  22351  dvcnvlem  22377  dvef  22381  rollelem  22390  dvlip2  22396  dvivthlem1  22409  dvivth  22411  lhop2  22416  lhop  22417  dvcnvrelem1  22418  dvcnvrelem2  22419  dvcnvre  22420  ply1rem  22564  fta1blem  22569  plycpn  22685  plyrem  22701  tayl0  22757  dvtaylp  22765  dvntaylp  22766  dvntaylp0  22767  taylthlem1  22768  taylthlem2  22769  ulmdvlem3  22797  psercn  22821  pserdv  22824  abelth  22836  efabl  22937  efopnlem1  23037  loglesqrt  23132  efrlim  23299  dchrghm  23531  dchrptlem3  23541  tgbtwntriv2  23878  tgbtwnne  23881  ercgrg  23908  tgidinside  23958  tgbtwnconn1  23962  tglnne  24008  tglnne0  24020  tglnpt2  24021  tglineneq  24024  ncolncol  24026  coltr3  24029  mirln  24056  mirln2  24057  mirconn  24058  krippenlem  24067  footex  24095  colperpexlem3  24106  mideulem2  24108  opphllem  24109  opphllem1  24119  opphllem2  24120  opphllem4  24122  opphl  24125  hpgerlem  24134  midbtwn  24145  lmieu  24150  lmiisolem  24161  f1otrg  24174  f1otrge  24175  ebtwntg  24285  ecgrtg  24286  eengtrkg  24288  eengtrkge  24289  nbgraop  24423  nbgraf1olem5  24445  wwlknext  24724  wwlkm1edg  24735  wwlkextproplem3  24743  clwwlkel  24793  vdgr1d  24903  vdgr1b  24904  eupap1  24976  extwwlkfablem2  25078  numclwwlkovf2ex  25086  numclwlk1lem2foa  25091  numclwwlk2lem1  25102  numclwlk2lem2f  25103  spansnid  26481  elspansn4  26491  submarchi  27730  qtopt1  27838  qtophaus  27839  locfinref  27844  ordtrest2NEWlem  27904  elzrhunit  27960  qqhcn  27972  qqhucn  27973  esumel  28058  esumsplit  28063  sigagenss2  28150  elsx  28165  sxbrsigalem0  28242  dya2icoseg  28248  eulerpartlemb  28307  eulerpartlemgvv  28315  iwrdsplit  28326  sseqfv2  28333  probfinmeasb  28368  dstrvprob  28410  dstfrvel  28412  ballotlemrv  28458  signstfvn  28526  signstfvp  28528  signstfveq0  28534  signsvtp  28540  signsvtn  28541  subfacp1lem5  28628  ptpcon  28678  indispcon  28679  cvxscon  28688  cvmseu  28721  cvmliftmolem2  28727  cvmliftlem7  28736  cvmliftlem10  28739  cvmliftlem13  28741  cvmlift2lem12  28759  mrsubcv  28870  mrsubff  28872  mrsubrn  28873  mrsubccat  28878  elmrsubrn  28880  mrsubco  28881  mrsubvrs  28882  mvhf  28918  msubvrs  28920  mclsax  28929  predfz  29283  linerflx1  29799  linerflx2  29801  elhf2  29832  opnmbllem0  30050  areacirclem2  30108  areacirclem4  30110  neibastop2lem  30178  blssp  30249  sstotbnd2  30270  totbndbnd  30285  prdstotbnd  30290  cnpwstotbnd  30293  heiborlem9  30315  exidcl  30338  exidresid  30341  grpokerinj  30347  iscringd  30396  prter3  30623  wepwsolem  30987  kercvrlsm  31029  dfacbasgrp  31057  cntzsdrg  31151  dvconstbi  31239  cncmpmax  31407  iooabslt  31532  fmul01lt1lem2  31579  limciccioolb  31627  limcicciooub  31643  fsumcncf  31680  ioccncflimc  31688  icocncflimc  31692  cncfiooicclem1  31696  dvbdfbdioolem2  31726  dvnmul  31740  stoweidlem26  31808  stoweidlem34  31816  stoweidlem48  31830  stoweidlem59  31841  dirkercncflem3  31887  fourierdlem32  31921  fourierdlem41  31930  fourierdlem51  31940  fourierdlem63  31952  fourierdlem82  31971  fourierdlem85  31974  fourierdlem93  31982  fourierdlem111  32000  fourierdlem114  32003  etransclem35  32052  fzoopth  32340  invisoinvl  32574  estrreslem2  32644  funcestrcsetclem3  32648  funcestrcsetclem8  32653  funcsetcestrclem3  32662  funcsetcestrclem8  32668  rnghmsubcsetclem1  32783  rngccatidOLD  32797  zrinitorngc  32808  zrtermorngc  32809  zrzeroorngc  32810  rhmsubcsetclem1  32829  rhmsubcrngclem1  32835  funcringcsetcOLD2lem3  32846  funcringcsetcOLD2lem8  32851  ringccatidOLD  32860  funcringcsetclem3OLD  32869  funcringcsetclem8OLD  32874  irinitoringc  32877  zrtermoringc  32878  zrninitoringc  32879  nzerooringczr  32880  srhmsubclem2  32882  srhmsubc  32884  srhmsubcOLDlem2  32901  srhmsubcOLD  32903  rhmsubcOLDlem3  32915  lcosslsp  33039  bnj1006  34017  bnj1018  34020  bnj1121  34041  bnj1398  34090  bnj1450  34106  bnj1501  34123  toycom  34698  islfld  34787  lshpsmreu  34834  ldualelvbase  34852  ldualssvscl  34883  lkreqN  34895  lkrlspeqN  34896  erng1lem  36713  erngdvlem4  36717  erng0g  36720  erng1r  36721  erngdvlem4-rN  36725  dva0g  36754  dia1dim2  36789  dia1dimid  36790  dia2dimlem5  36795  dvhelvbasei  36815  dvhvaddass  36824  tendoinvcl  36831  tendolinv  36832  tendorinv  36833  dvhgrp  36834  dvhlveclem  36835  cdlemn4  36925  lcfrlem12N  37281  lcfrlem15  37284  lcdvscl  37332  lcdlssvscl  37333  lcdvsass  37334  lcdvs0N  37343  mapdincl  37388  mapdin  37389  mapdlsmcl  37390  mapdcnvatN  37393  mapdpglem2  37400  mapdpglem12  37410  mapdpglem18  37416  mapdpglem21  37419  mapdpglem22  37420  mapdpglem28  37428  mapdpglem30  37429  hdmaprnlem3N  37580  hdmaprnlem3uN  37581  hdmaprnlem7N  37585  hdmaprnlem8N  37586  hdmaprnlem9N  37587  hdmaprnlem3eN  37588  hdmaprnlem16N  37592  hgmapdcl  37620  hgmapval1  37623  hgmaprnlem4N  37629  hdmapinvlem1  37648  imo72b2lem0  37982
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