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

Theorem eleqtrd 2359
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 2350 . 2  |-  ( ph  ->  ( A  e.  B  <->  A  e.  C ) )
41, 3mpbid 201 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  eleqtrrd  2360  3eltr3d  2363  syl5eleq  2369  syl6eleq  2373  opth1  4244  0nelop  4256  tfisi  4649  fviss  5580  fnwelem  6230  omeulem1  6580  oeeulem  6599  oeeui  6600  oaabs2  6643  omabs  6645  ercl  6671  erth  6704  ecelqsdm  6729  ordtypelem6  7238  ordtypelem7  7239  cantnfval  7369  cantnfp1lem3  7382  cantnflem4  7394  r1pwss  7456  rankonidlem  7500  rankxplim3  7551  fseqenlem2  7652  iunfictbso  7741  dfac12lem1  7769  dfac12lem2  7770  fin23lem30  7968  iundom2g  8162  fpwwe2lem6  8257  fpwwe2lem9  8260  icoshftf1o  10759  lincmb01cmp  10777  fzopth  10828  fzoaddel2  10907  fzosubel2  10909  fzoend  10914  peano2fzor  10919  monoord2  11077  sermono  11078  expmulnbnd  11233  bcpasc  11333  ccatcl  11429  swrdcl  11452  revcl  11479  revlen  11480  fsum0diag2  12245  isumsplit  12299  sadadd  12658  sadass  12662  smuval2  12673  smumul  12684  vdwapun  13021  vdwlem9  13036  ramub1lem1  13073  prdsbasfn  13370  prdsbasprj  13371  pwsplusgval  13389  pwsmulrval  13390  pwsvscafval  13393  xpsaddlem  13477  xpsvsca  13481  xpsle  13483  mreexmrid  13545  homfeqval  13600  comfval2  13606  comfeq  13609  comfeqval  13611  oppccomfpropd  13630  invco  13673  sectepi  13682  issubc3  13723  funcf2  13742  funciso  13748  fthepi  13802  nat1st2nd  13825  fuciso  13849  homarcl2  13867  coapm  13903  setcmon  13919  setcepi  13920  setcsect  13921  setcinv  13922  setciso  13923  catccatid  13934  resscatc  13937  catciso  13939  catcoppccl  13940  catcfuccl  13941  xpccatid  13962  catcxpccl  13981  xpcpropd  13982  evlfcl  13996  curfpropd  14007  hofcl  14033  yonedalem3  14054  yonffthlem  14056  poslubdg  14252  grpidd  14395  ismndd  14396  mndpropd  14398  issubmnd  14401  submnd0  14402  imasmnd  14410  gsumress  14454  frmdelbas  14475  grpidd2  14519  submmulg  14602  pwsinvg  14607  imasgrp  14611  subginvcl  14630  subgcl  14631  subgsub  14633  subgmulg  14635  divseccl  14673  gaid2  14757  submod  14880  odsubdvds  14882  sylow1lem4  14912  sylow2alem2  14929  lsmdisj2  14991  subgdisj1  15000  pj1id  15008  efgsrel  15043  efgrelexlemb  15059  efgcpbl2  15066  frgpcpbl  15068  frgp0  15069  frgpeccl  15070  frgpadd  15072  frgpup3lem  15086  frgpnabllem1  15161  cycsubgcyg  15187  prdsgsum  15229  dprdfeq0  15257  dmdprdsplitlem  15272  dpjidcl  15293  pgpfac1lem3a  15311  pgpfac1lem4  15313  pgpfaclem1  15316  pgpfaclem2  15317  ablfaclem2  15321  rngidss  15367  rngpropd  15372  imasrng  15402  divsrng2  15403  subrg1  15555  subrgmcl  15557  subrgdv  15562  subrgunit  15563  issubdrg  15570  resrhm  15574  lmodprop2d  15687  0lmhm  15797  lmhmpropd  15826  lspprabs  15848  lspfixed  15881  lssacsex  15897  lbsextlem4  15914  divscrng  15992  assapropd  16067  psrelbas  16125  resspsrvsca  16162  subrgpsr  16163  mplcoe1  16209  mplbas2  16212  mplascl  16237  mplmon2cl  16241  mplmon2mul  16242  vr1cl2  16272  ply1lss  16275  ply1subrg  16276  psropprmul  16316  znf1o  16505  elocv  16568  pjff  16612  elcls3  16820  mreclatdemo  16833  resstps  16917  ordtrest2lem  16933  ordtrest2  16934  pnfnei  16950  mnfnei  16951  iscnp2  16969  cnrest2r  17015  lmcls  17030  lmcld  17031  cnt0  17074  cnhaus  17082  isreg2  17105  conclo  17141  1stccnp  17188  loclly  17213  lly1stc  17222  kgencmp2  17241  llycmpkgen2  17245  kgen2ss  17250  kgencn3  17253  pttoponconst  17292  txcls  17299  txbasval  17301  dfac14lem  17311  ptcn  17321  ptrescn  17333  txtube  17334  txcmplem1  17335  txlm  17342  txkgen  17346  xkopjcn  17350  cnmpt2res  17371  cnmptkp  17374  xkoinjcn  17381  qtopkgen  17401  imastps  17412  isr0  17428  r0cld  17429  pt1hmeo  17497  ptuncnv  17498  ptunhmeo  17499  filintn0  17556  trnei  17587  flimfil  17664  flimopn  17670  fbflim2  17672  cnpflf2  17695  flfcnp  17699  flfcnp2  17702  fclsopn  17709  fcfnei  17730  cnpfcf  17736  alexsublem  17738  ptcmplem3  17748  ptcmplem4  17749  tmdcn2  17772  tmdgsum  17778  tmdgsum2  17779  symgtgp  17784  tgphaus  17799  tgpt1  17800  divstgplem  17803  prdstmdd  17806  prdstgpd  17807  haustsms  17818  tsmscls  17820  tsmsmhm  17828  tsmsadd  17829  tgptsmscls  17832  tsmssplit  17834  xmetunirn  17902  ressprdsds  17935  xpsdsval  17945  blbas  17976  mopntopon  17985  isxms2  17994  imasf1oxms  18035  imasf1oms  18036  ressxms  18071  ressms  18072  prdsxmslem2  18075  tmsxpsval  18084  tngngp2  18168  tngngp  18170  tgioo  18302  metdseq0  18358  cncfmpt2f  18418  cncfcnvcn  18424  cnmptre  18425  cnheibor  18453  nmhmcn  18601  cphsubrglem  18613  cphreccllem  18614  iscmet3  18719  relcmpcmet  18742  bcthlem4  18749  minveclem4  18796  ivthicc  18818  evthicc  18819  ovolicc2lem4  18879  ovolicc2lem5  18880  iunmbl2  18914  vitalilem3  18965  cncombf  19013  cnmbf  19014  limcco  19243  dvres2lem  19260  cpncn  19285  cpnres  19286  dvaddbr  19287  dvmulbr  19288  dvcobr  19295  dvcjbr  19298  dvrec  19304  dvcnvlem  19323  dvlip2  19342  dvivth  19357  lhop2  19362  lhop  19363  dvcnvrelem1  19364  dvcnvrelem2  19365  dvcnvre  19366  ftc1lem6  19388  evlrhm  19409  evl1vsd  19420  evl1expd  19421  mpfconst  19422  mdegvscale  19461  mdegvsca  19462  fta1blem  19554  plyaddlem1  19595  plymullem1  19596  coeeulem  19606  tayl0  19741  taylthlem1  19752  taylthlem2  19753  ulmdvlem3  19779  psercnlem2  19800  psercn  19802  cxpcn3  20088  loglesqr  20098  efrlim  20264  jensen  20283  ppinprm  20390  chtnprm  20392  dchrptlem1  20503  dchrptlem2  20504  grpoidinv2  20885  grpoinv  20894  ubthlem2  21450  shuni  21879  lmxrge0  23375  gsumpropd2lem  23379  esumadd  23432  esumaddf  23434  esumcocn  23448  mbfmco2  23570  indispcon  23765  conpcon  23766  pconpi1  23768  sconpi1  23770  cvmsss2  23805  cvmliftmolem1  23812  cvmliftlem8  23823  cvmliftlem10  23825  cvmliftlem11  23826  cvmlift2lem9  23842  cvmlift2lem12  23845  cvmlift3lem7  23856  eupap1  23900  axlowdimlem16  24585  linethru  24776  areacirclem5  24929  pre2befi2  25232  iscnp4  25563  cnpflf4  25564  limhun  25570  prdnei  25573  altretop  25600  homib  25796  isibg1a6  26125  isibg1a7  26126  isibg1a8  26127  ivthALT  26258  locfincmp  26304  comppfsc  26307  neibastop2  26310  filnetlem4  26330  fdc  26455  isbnd3  26508  prdsbnd  26517  prdstotbnd  26518  prdsbnd2  26519  rrnequiv  26559  reheibor  26563  iscringd  26624  isfldidl  26693  diophin  26852  acongeq  27070  frlmlss  27219  frlmvscafval  27230  uvcresum  27242  frlmssuvc1  27246  frlmssuvc2  27247  frlmsslsp  27248  frlmup1  27250  isnumbasgrplem2  27269  psgnunilem1  27416  psgnghm2  27438  matrng  27480  matassa  27481  mat1  27482  proot1mul  27515  stoweidlem26  27775  stoweidlem27  27776  stoweidlem31  27780  stoweidlem34  27783  stirlinglem14  27836  bnj1450  29080  bnj1501  29097  eqlkr  29289  ldualvsubval  29347  dvalveclem  31215  dia2dimlem5  31258  dia2dimlem9  31262  tendoinvcl  31294  dvhgrp  31297  dvhlveclem  31298  dihpN  31526  dochsnkr2cl  31664  lcfl7lem  31689  lclkr  31723  lclkrs  31729  lcfrvalsnN  31731  lcfrlem4  31735  lcfrlem6  31737  lcfrlem16  31748  lcdvsubval  31808  lcdlkreqN  31812  mapdcl2  31846  mapdincl  31851  mapdlsmcl  31853  mapdpglem3  31865  hdmaprnlem9N  32050  hdmaplkr  32106  hdmapip0  32108  hdmapglem7a  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator