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

Theorem eleqtrd 2512
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eleqtrd.1  |-  ( ph  ->  A  e.  B )
eleqtrd.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
eleqtrd  |-  ( ph  ->  A  e.  C )

Proof of Theorem eleqtrd
StepHypRef Expression
1 eleqtrd.1 . 2  |-  ( ph  ->  A  e.  B )
2 eleqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32eleq2d 2503 . 2  |-  ( ph  ->  ( A  e.  B  <->  A  e.  C ) )
41, 3mpbid 202 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725
This theorem is referenced by:  eleqtrrd  2513  3eltr3d  2516  syl5eleq  2522  syl6eleq  2526  opth1  4434  0nelop  4446  suctr  4665  tfisi  4838  fviss  5784  fnwelem  6461  omeulem1  6825  oeeulem  6844  oeeui  6845  oaabs2  6888  omabs  6890  ercl  6916  erth  6949  ecelqsdm  6974  ordtypelem6  7492  ordtypelem7  7493  cantnfval  7623  cantnfp1lem3  7636  cantnflem4  7648  r1pwss  7710  rankonidlem  7754  rankxplim3  7805  fseqenlem2  7906  iunfictbso  7995  dfac12lem1  8023  dfac12lem2  8024  fin23lem30  8222  iundom2g  8415  fpwwe2lem6  8510  fpwwe2lem9  8513  lincmb01cmp  11038  fzopth  11089  fzoaddel2  11176  fzosubel2  11178  fzoend  11187  peano2fzor  11194  monoord2  11354  sermono  11355  expmulnbnd  11511  bcpasc  11612  ccatcl  11743  swrdcl  11766  revcl  11793  revlen  11794  fsum0diag2  12566  isumsplit  12620  sadadd  12979  sadass  12983  smuval2  12994  smumul  13005  vdwapun  13342  vdwlem9  13357  ramub1lem1  13394  prdsbasfn  13693  prdsbasprj  13694  pwsplusgval  13712  pwsmulrval  13713  pwsvscafval  13716  xpsaddlem  13800  xpsvsca  13804  xpsle  13806  mreexmrid  13868  homfeqval  13923  comfval2  13929  comfeq  13932  comfeqval  13934  oppccomfpropd  13953  invco  13996  sectepi  14005  issubc3  14046  funcf2  14065  funciso  14071  fthepi  14125  nat1st2nd  14148  fuciso  14172  homarcl2  14190  coapm  14226  setcmon  14242  setcepi  14243  setcsect  14244  setcinv  14245  setciso  14246  catccatid  14257  resscatc  14260  catciso  14262  catcoppccl  14263  catcfuccl  14264  xpccatid  14285  catcxpccl  14304  xpcpropd  14305  evlfcl  14319  curfpropd  14330  hofcl  14356  yonedalem3  14377  yonffthlem  14379  poslubdg  14575  grpidd  14718  ismndd  14719  mndpropd  14721  issubmnd  14724  submnd0  14725  imasmnd  14733  gsumress  14777  frmdelbas  14798  grpidd2  14842  submmulg  14925  pwsinvg  14930  imasgrp  14934  subginvcl  14953  subgcl  14954  subgsub  14956  subgmulg  14958  divseccl  14996  gaid2  15080  submod  15203  odsubdvds  15205  sylow1lem4  15235  sylow2alem2  15252  lsmdisj2  15314  subgdisj1  15323  pj1id  15331  efgsrel  15366  efgrelexlemb  15382  efgcpbl2  15389  frgpcpbl  15391  frgp0  15392  frgpeccl  15393  frgpadd  15395  frgpup3lem  15409  frgpnabllem1  15484  cycsubgcyg  15510  prdsgsum  15552  dprdfeq0  15580  dmdprdsplitlem  15595  dpjidcl  15616  pgpfac1lem3a  15634  pgpfac1lem4  15636  pgpfaclem1  15639  pgpfaclem2  15640  ablfaclem2  15644  rngidss  15690  rngpropd  15695  imasrng  15725  divsrng2  15726  subrg1  15878  subrgmcl  15880  subrgdv  15885  subrgunit  15886  issubdrg  15893  resrhm  15897  lmodprop2d  16006  0lmhm  16116  lmhmpropd  16145  lspfixed  16200  lssacsex  16216  lbsextlem4  16233  divscrng  16311  assapropd  16386  psrelbas  16444  resspsrvsca  16481  subrgpsr  16482  mplcoe1  16528  mplbas2  16531  mplascl  16556  mplmon2cl  16560  mplmon2mul  16561  vr1cl2  16591  ply1lss  16594  ply1subrg  16595  psropprmul  16632  znf1o  16832  elocv  16895  pjff  16939  elcls3  17147  mreclatdemo  17160  neiptopnei  17196  resstps  17251  ordtrest2lem  17267  ordtrest2  17268  pnfnei  17284  mnfnei  17285  iscnp2  17303  iscnp4  17327  cnrest2r  17351  lmcls  17366  lmcld  17367  cnt0  17410  cnhaus  17418  isreg2  17441  conclo  17478  1stccnp  17525  loclly  17550  lly1stc  17559  kgencmp2  17578  llycmpkgen2  17582  kgen2ss  17587  kgencn3  17590  pttoponconst  17629  txcls  17636  txbasval  17638  dfac14lem  17649  ptcn  17659  ptrescn  17671  txtube  17672  txcmplem1  17673  txlm  17680  txkgen  17684  xkopjcn  17688  cnmptkp  17712  xkoinjcn  17719  qtopkgen  17742  imastps  17753  isr0  17769  r0cld  17770  pt1hmeo  17838  ptuncnv  17839  ptunhmeo  17840  filintn0  17893  trnei  17924  flimfil  18001  flimopn  18007  fbflim2  18009  cnpflf2  18032  flfcnp  18036  flfcnp2  18039  fclsopn  18046  fcfnei  18067  cnpfcf  18073  alexsublem  18075  ptcmplem3  18085  ptcmplem4  18086  cnextfres  18099  tmdcn2  18119  tmdgsum  18125  tmdgsum2  18126  symgtgp  18131  tgphaus  18146  tgpt1  18147  divstgplem  18150  prdstmdd  18153  prdstgpd  18154  haustsms  18165  tsmscls  18167  tsmsmhm  18175  tsmsadd  18176  tgptsmscls  18179  tsmssplit  18181  restutop  18267  utopreg  18282  ressusp  18295  ucncn  18315  xmetunirn  18367  ressprdsds  18401  xpsdsval  18411  xblss2ps  18431  blbas  18460  mopntopon  18469  isxms2  18478  imasf1oxms  18519  imasf1oms  18520  prdsxmslem2  18559  tmsxpsval  18568  tngngp2  18693  tngngp  18695  tgioo  18827  metdseq0  18884  cncfmpt2f  18944  cncfcnvcn  18951  cnmptre  18952  cnheibor  18980  nmhmcn  19128  cphsubrglem  19140  cphreccllem  19141  iscmet3  19246  relcmpcmet  19269  bcthlem4  19280  minveclem4  19333  ivthicc  19355  evthicc  19356  ovolicc2lem4  19416  ovolicc2lem5  19417  iunmbl2  19451  vitalilem3  19502  cncombf  19550  cnmbf  19551  dvres2lem  19797  cpncn  19822  cpnres  19823  dvaddbr  19824  dvmulbr  19825  dvcobr  19832  dvcjbr  19835  dvrec  19841  dvcnvlem  19860  dvlip2  19879  dvivth  19894  lhop2  19899  lhop  19900  dvcnvrelem1  19901  dvcnvrelem2  19902  dvcnvre  19903  ftc1lem6  19925  evlrhm  19946  evl1vsd  19957  evl1expd  19958  mpfconst  19959  mdegvscale  19998  mdegvsca  19999  fta1blem  20091  plyaddlem1  20132  plymullem1  20133  coeeulem  20143  tayl0  20278  taylthlem1  20289  taylthlem2  20290  ulmdvlem3  20318  psercnlem2  20340  psercn  20342  cxpcn3  20632  loglesqr  20642  efrlim  20808  ppinprm  20935  chtnprm  20937  dchrptlem1  21048  dchrptlem2  21049  eupap1  21698  grpoidinv2  21806  grpoinv  21815  ubthlem2  22373  shuni  22802  kerf1hrm  24262  lmxrge0  24337  nmmulg  24352  rrhcn  24380  esumadd  24448  esumaddf  24453  esumcocn  24470  measiuns  24571  mbfmco2  24615  dya2iocnrect  24631  sibf0  24649  sibfof  24654  indispcon  24921  conpcon  24922  pconpi1  24924  sconpi1  24926  cvmsss2  24961  cvmliftmolem1  24968  cvmliftlem8  24979  cvmliftlem10  24981  cvmliftlem11  24982  cvmlift2lem9  24998  cvmlift2lem12  25001  cvmlift3lem7  25012  fprodser  25275  axlowdimlem16  25896  linethru  26087  areacirclem4  26295  ivthALT  26338  locfincmp  26384  comppfsc  26387  neibastop2  26390  filnetlem4  26410  fdc  26449  isbnd3  26493  prdsbnd  26502  prdstotbnd  26503  prdsbnd2  26504  rrnequiv  26544  reheibor  26548  iscringd  26609  isfldidl  26678  diophin  26831  acongeq  27048  frlmlss  27196  frlmvscafval  27207  uvcresum  27219  frlmssuvc1  27223  frlmssuvc2  27224  frlmsslsp  27225  frlmup1  27227  isnumbasgrplem2  27246  psgnghm2  27415  matrng  27457  matassa  27458  mat1  27459  proot1mul  27492  stoweidlem26  27751  stoweidlem27  27752  stoweidlem31  27756  stoweidlem34  27759  el2fzo  28138  fzoopth  28139  bnj1450  29419  bnj1501  29436  eqlkr  29897  ldualvsubval  29955  dvalveclem  31823  dia2dimlem5  31866  dia2dimlem9  31870  tendoinvcl  31902  dvhgrp  31905  dvhlveclem  31906  dihpN  32134  dochsnkr2cl  32272  lcfl7lem  32297  lclkr  32331  lclkrs  32337  lcfrvalsnN  32339  lcfrlem4  32343  lcfrlem6  32345  lcfrlem16  32356  lcdvsubval  32416  lcdlkreqN  32420  mapdcl2  32454  mapdincl  32459  mapdlsmcl  32461  mapdpglem3  32473  hdmaprnlem9N  32658  hdmaplkr  32714  hdmapip0  32716  hdmapglem7a  32728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator