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

Theorem eleqtrd 2372
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 2363 . 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 1632    e. wcel 1696
This theorem is referenced by:  eleqtrrd  2373  3eltr3d  2376  syl5eleq  2382  syl6eleq  2386  opth1  4260  0nelop  4272  tfisi  4665  fviss  5596  fnwelem  6246  omeulem1  6596  oeeulem  6615  oeeui  6616  oaabs2  6659  omabs  6661  ercl  6687  erth  6720  ecelqsdm  6745  ordtypelem6  7254  ordtypelem7  7255  cantnfval  7385  cantnfp1lem3  7398  cantnflem4  7410  r1pwss  7472  rankonidlem  7516  rankxplim3  7567  fseqenlem2  7668  iunfictbso  7757  dfac12lem1  7785  dfac12lem2  7786  fin23lem30  7984  iundom2g  8178  fpwwe2lem6  8273  fpwwe2lem9  8276  icoshftf1o  10775  lincmb01cmp  10793  fzopth  10844  fzoaddel2  10923  fzosubel2  10925  fzoend  10930  peano2fzor  10935  monoord2  11093  sermono  11094  expmulnbnd  11249  bcpasc  11349  ccatcl  11445  swrdcl  11468  revcl  11495  revlen  11496  fsum0diag2  12261  isumsplit  12315  sadadd  12674  sadass  12678  smuval2  12689  smumul  12700  vdwapun  13037  vdwlem9  13052  ramub1lem1  13089  prdsbasfn  13386  prdsbasprj  13387  pwsplusgval  13405  pwsmulrval  13406  pwsvscafval  13409  xpsaddlem  13493  xpsvsca  13497  xpsle  13499  mreexmrid  13561  homfeqval  13616  comfval2  13622  comfeq  13625  comfeqval  13627  oppccomfpropd  13646  invco  13689  sectepi  13698  issubc3  13739  funcf2  13758  funciso  13764  fthepi  13818  nat1st2nd  13841  fuciso  13865  homarcl2  13883  coapm  13919  setcmon  13935  setcepi  13936  setcsect  13937  setcinv  13938  setciso  13939  catccatid  13950  resscatc  13953  catciso  13955  catcoppccl  13956  catcfuccl  13957  xpccatid  13978  catcxpccl  13997  xpcpropd  13998  evlfcl  14012  curfpropd  14023  hofcl  14049  yonedalem3  14070  yonffthlem  14072  poslubdg  14268  grpidd  14411  ismndd  14412  mndpropd  14414  issubmnd  14417  submnd0  14418  imasmnd  14426  gsumress  14470  frmdelbas  14491  grpidd2  14535  submmulg  14618  pwsinvg  14623  imasgrp  14627  subginvcl  14646  subgcl  14647  subgsub  14649  subgmulg  14651  divseccl  14689  gaid2  14773  submod  14896  odsubdvds  14898  sylow1lem4  14928  sylow2alem2  14945  lsmdisj2  15007  subgdisj1  15016  pj1id  15024  efgsrel  15059  efgrelexlemb  15075  efgcpbl2  15082  frgpcpbl  15084  frgp0  15085  frgpeccl  15086  frgpadd  15088  frgpup3lem  15102  frgpnabllem1  15177  cycsubgcyg  15203  prdsgsum  15245  dprdfeq0  15273  dmdprdsplitlem  15288  dpjidcl  15309  pgpfac1lem3a  15327  pgpfac1lem4  15329  pgpfaclem1  15332  pgpfaclem2  15333  ablfaclem2  15337  rngidss  15383  rngpropd  15388  imasrng  15418  divsrng2  15419  subrg1  15571  subrgmcl  15573  subrgdv  15578  subrgunit  15579  issubdrg  15586  resrhm  15590  lmodprop2d  15703  0lmhm  15813  lmhmpropd  15842  lspprabs  15864  lspfixed  15897  lssacsex  15913  lbsextlem4  15930  divscrng  16008  assapropd  16083  psrelbas  16141  resspsrvsca  16178  subrgpsr  16179  mplcoe1  16225  mplbas2  16228  mplascl  16253  mplmon2cl  16257  mplmon2mul  16258  vr1cl2  16288  ply1lss  16291  ply1subrg  16292  psropprmul  16332  znf1o  16521  elocv  16584  pjff  16628  elcls3  16836  mreclatdemo  16849  resstps  16933  ordtrest2lem  16949  ordtrest2  16950  pnfnei  16966  mnfnei  16967  iscnp2  16985  cnrest2r  17031  lmcls  17046  lmcld  17047  cnt0  17090  cnhaus  17098  isreg2  17121  conclo  17157  1stccnp  17204  loclly  17229  lly1stc  17238  kgencmp2  17257  llycmpkgen2  17261  kgen2ss  17266  kgencn3  17269  pttoponconst  17308  txcls  17315  txbasval  17317  dfac14lem  17327  ptcn  17337  ptrescn  17349  txtube  17350  txcmplem1  17351  txlm  17358  txkgen  17362  xkopjcn  17366  cnmpt2res  17387  cnmptkp  17390  xkoinjcn  17397  qtopkgen  17417  imastps  17428  isr0  17444  r0cld  17445  pt1hmeo  17513  ptuncnv  17514  ptunhmeo  17515  filintn0  17572  trnei  17603  flimfil  17680  flimopn  17686  fbflim2  17688  cnpflf2  17711  flfcnp  17715  flfcnp2  17718  fclsopn  17725  fcfnei  17746  cnpfcf  17752  alexsublem  17754  ptcmplem3  17764  ptcmplem4  17765  tmdcn2  17788  tmdgsum  17794  tmdgsum2  17795  symgtgp  17800  tgphaus  17815  tgpt1  17816  divstgplem  17819  prdstmdd  17822  prdstgpd  17823  haustsms  17834  tsmscls  17836  tsmsmhm  17844  tsmsadd  17845  tgptsmscls  17848  tsmssplit  17850  xmetunirn  17918  ressprdsds  17951  xpsdsval  17961  blbas  17992  mopntopon  18001  isxms2  18010  imasf1oxms  18051  imasf1oms  18052  ressxms  18087  ressms  18088  prdsxmslem2  18091  tmsxpsval  18100  tngngp2  18184  tngngp  18186  tgioo  18318  metdseq0  18374  cncfmpt2f  18434  cncfcnvcn  18440  cnmptre  18441  cnheibor  18469  nmhmcn  18617  cphsubrglem  18629  cphreccllem  18630  iscmet3  18735  relcmpcmet  18758  bcthlem4  18765  minveclem4  18812  ivthicc  18834  evthicc  18835  ovolicc2lem4  18895  ovolicc2lem5  18896  iunmbl2  18930  vitalilem3  18981  cncombf  19029  cnmbf  19030  limcco  19259  dvres2lem  19276  cpncn  19301  cpnres  19302  dvaddbr  19303  dvmulbr  19304  dvcobr  19311  dvcjbr  19314  dvrec  19320  dvcnvlem  19339  dvlip2  19358  dvivth  19373  lhop2  19378  lhop  19379  dvcnvrelem1  19380  dvcnvrelem2  19381  dvcnvre  19382  ftc1lem6  19404  evlrhm  19425  evl1vsd  19436  evl1expd  19437  mpfconst  19438  mdegvscale  19477  mdegvsca  19478  fta1blem  19570  plyaddlem1  19611  plymullem1  19612  coeeulem  19622  tayl0  19757  taylthlem1  19768  taylthlem2  19769  ulmdvlem3  19795  psercnlem2  19816  psercn  19818  cxpcn3  20104  loglesqr  20114  efrlim  20280  jensen  20299  ppinprm  20406  chtnprm  20408  dchrptlem1  20519  dchrptlem2  20520  grpoidinv2  20901  grpoinv  20910  ubthlem2  21466  shuni  21895  lmxrge0  23390  gsumpropd2lem  23394  esumadd  23447  esumaddf  23449  esumcocn  23463  mbfmco2  23585  indispcon  23780  conpcon  23781  pconpi1  23783  sconpi1  23785  cvmsss2  23820  cvmliftmolem1  23827  cvmliftlem8  23838  cvmliftlem10  23840  cvmliftlem11  23841  cvmlift2lem9  23857  cvmlift2lem12  23860  cvmlift3lem7  23871  eupap1  23915  axlowdimlem16  24657  linethru  24848  areacirclem5  25032  pre2befi2  25335  iscnp4  25666  cnpflf4  25667  limhun  25673  prdnei  25676  altretop  25703  homib  25899  isibg1a6  26228  isibg1a7  26229  isibg1a8  26230  ivthALT  26361  locfincmp  26407  comppfsc  26410  neibastop2  26413  filnetlem4  26433  fdc  26558  isbnd3  26611  prdsbnd  26620  prdstotbnd  26621  prdsbnd2  26622  rrnequiv  26662  reheibor  26666  iscringd  26727  isfldidl  26796  diophin  26955  acongeq  27173  frlmlss  27322  frlmvscafval  27333  uvcresum  27345  frlmssuvc1  27349  frlmssuvc2  27350  frlmsslsp  27351  frlmup1  27353  isnumbasgrplem2  27372  psgnunilem1  27519  psgnghm2  27541  matrng  27583  matassa  27584  mat1  27585  proot1mul  27618  stoweidlem26  27878  stoweidlem27  27879  stoweidlem31  27883  stoweidlem34  27886  stirlinglem14  27939  bnj1450  29396  bnj1501  29413  eqlkr  29911  ldualvsubval  29969  dvalveclem  31837  dia2dimlem5  31880  dia2dimlem9  31884  tendoinvcl  31916  dvhgrp  31919  dvhlveclem  31920  dihpN  32148  dochsnkr2cl  32286  lcfl7lem  32311  lclkr  32345  lclkrs  32351  lcfrvalsnN  32353  lcfrlem4  32357  lcfrlem6  32359  lcfrlem16  32370  lcdvsubval  32430  lcdlkreqN  32434  mapdcl2  32468  mapdincl  32473  mapdlsmcl  32475  mapdpglem3  32487  hdmaprnlem9N  32672  hdmaplkr  32728  hdmapip0  32730  hdmapglem7a  32742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator