MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeltrdi Structured version   Visualization version   GIF version

Theorem eqeltrdi 2920
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
eqeltrdi.1 (𝜑𝐴 = 𝐵)
eqeltrdi.2 𝐵𝐶
Assertion
Ref Expression
eqeltrdi (𝜑𝐴𝐶)

Proof of Theorem eqeltrdi
StepHypRef Expression
1 eqeltrdi.1 . 2 (𝜑𝐴 = 𝐵)
2 eqeltrdi.2 . . 3 𝐵𝐶
32a1i 11 . 2 (𝜑𝐵𝐶)
41, 3eqeltrd 2912 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2814  df-clel 2892
This theorem is referenced by:  eqeltrrdi  2921  csbexg  5187  unisn2  5189  class2set  5227  snexALT  5257  snex  5305  prex  5306  onun2i  6279  iotaex  6308  fvrn0  6671  f0cli  6837  funsneqopb  6887  fmptsng  6903  fmptsnd  6904  elimdelov  7224  ovima0  7302  ndmovcl  7308  caovmo  7360  soex  7601  zfrep6  7631  1st2ndb  7704  wfrlem17  7946  smofvon2  7968  tz7.44-2  8018  oesuclem  8125  omcl  8136  oecl  8137  nnmcl  8213  nnecl  8214  ixpexg  8461  resixpfo  8475  en1b  8552  xpsnen  8576  nnunifi  8745  xpfi  8765  fsuppun  8828  0fsupp  8831  oiexg  8975  hartogslem1  8982  cantnfvalf  9104  rankdmr1  9206  rankr1c  9226  numwdom  9462  alephon  9472  isfin5  9698  sdom2en01  9701  isf32lem9  9760  hsmexlem9  9824  iundom2g  9939  gchxpidm  10068  r1tskina  10181  tskmcl  10240  recmulnq  10363  recclnq  10365  genpelv  10399  un0mulcl  11909  znegcl  11995  zeo  12046  eqreznegel  12312  xnegcl  12584  xnn0xaddcl  12606  ioorebas  12819  modid0  13248  2txmodxeq0  13282  fzofi  13325  seqexw  13368  expcllem  13424  m1expcl2  13435  faclbnd4lem3  13639  bccl  13666  hasheq0  13708  hashrabrsn  13717  fnfz0hashnn0  13790  fnfzo0hashnn0  13793  wrdnfi  13879  ccat2s1p1OLD  13966  cshwcl  14139  relexpaddg  14391  abs00bd  14630  iserge0  14996  sumrblem  15047  fsumcvg  15048  summolem2a  15051  sumss  15060  fsumss  15061  fsumcvg2  15063  sumsplit  15102  binom  15164  bcxmas  15169  geomulcvg  15211  prodrblem  15262  fprodcvg  15263  prodmolem2a  15267  zprod  15270  fprodntriv  15275  prodss  15280  fprodss  15281  binomfallfac  15374  bpoly1  15384  bpoly2  15390  bpoly3  15391  ruclem6  15567  smupf  15804  gcdcl  15832  lcmcl  15922  lcmfcl  15949  2mulprm  16014  pcxcl  16174  pcmptcl  16204  infpnlem2  16224  zgz  16246  4sqlem2  16262  4sqlem19  16276  vdwapval  16286  hashbc0  16318  ramcl2  16329  0ramcl  16336  ramcl  16342  isstruct2  16472  imasval  16763  imasbas  16764  imasds  16765  imasplusg  16769  imasmulr  16770  imasvsca  16772  imasip  16773  imasle  16775  qusaddvallem  16803  qusaddflem  16804  qusaddval  16805  qusaddf  16806  qusmulval  16807  qusmulf  16808  mreexexlem3d  16896  sscpwex  17064  fullresc  17100  estrres  17368  evlfcl  17451  ipopos  17749  gsumress  17871  submnd0  17919  qusgrp2  18196  mulgfval  18205  issubg2  18273  triv1nsgd  18304  torsubg  18953  frgpnabllem1  18972  lt6abl  18994  ablfaclem3  19188  ablfac2  19190  simpgnsgd  19201  srgbinomlem3  19271  ringidss  19306  qusring2  19349  isdrngd  19503  mptscmfsupp0  19675  islss3  19707  lspsnel  19751  lspprel  19842  znf1o  20674  frgpcyg  20696  cnmsgnsubg  20697  phlpropd  20775  cssval  20802  iscss  20803  dsmm0cl  20860  uvcvvcl  20907  m1detdiag  21182  m2detleiblem1  21209  pmatcollpw3fi1lem1  21370  indistopon  21585  indiscld  21675  restbas  21742  ordttopon  21777  iocpnfordt  21799  icomnfordt  21800  lecldbas  21803  fiuncmp  21988  cmpfi  21992  conncompid  22015  dissnlocfin  22113  elpt  22156  xkotop  22172  xkouni  22183  xkohaus  22237  xkoptsub  22238  imastopn  22304  filconn  22467  cfinufil  22512  alexsublem  22628  alexsub  22629  alexsubALTlem4  22634  distgp  22683  indistgp  22684  ssblps  23008  ssbl  23009  xmeter  23019  nmoi  23313  nmoeq0  23321  0nghm  23326  idnghm  23328  icccld  23351  iocmnfcld  23353  blssioo  23379  xrtgioo  23390  xrsxmet  23393  icccmp  23409  pcopt  23606  pcopt2  23607  elpi1  23629  cmetcaulem  23871  ishl2  23953  rrxmvallem  23987  ovolcl  24061  ovolunlem1a  24079  ovolunnul  24083  ovoliunnul  24090  ioombl1  24145  icombl  24147  ioombl  24148  iccmbl  24149  iccvolcl  24150  ovolioo  24151  ioovolcl  24153  ioorcl  24160  uniioovol  24162  uniioombllem2a  24165  uniioombllem4  24169  uniioombllem5  24170  vitalilem1  24191  vitalilem5  24195  mbfconstlem  24210  mbfima  24213  mbfid  24218  ismbf2d  24223  mbfss  24229  mbfmulc2lem  24230  i1fd  24264  itg1addlem2  24280  itg1addlem4  24282  itg1addlem5  24283  i1fmulc  24286  itg2l  24312  itg2cl  24315  ibl0  24369  iblrelem  24373  iblpos  24375  iblss2  24388  bddmulibl  24421  bddiblnc  24424  recnperf  24487  ply1remlem  24742  fta1glem1  24745  fta1g  24747  elply  24771  plypf1  24788  coefv0  24824  coemulc  24831  fta1  24883  elqaalem2  24895  aannenlem2  24904  aalioulem3  24909  taylfvallem1  24931  tayl0  24936  ulm0  24965  logtayl  25230  atanrecl  25476  atanbnd  25491  harmonicbnd3  25572  ftalem7  25643  basellem5  25649  ppifi  25670  sqff1o  25746  1sgmprm  25762  logexprlim  25788  dchrelbasd  25802  dchr1re  25826  lgslem4  25863  lgsne0  25898  2sqlem9  25990  2sqlem10  25991  rpvmasumlem  26050  dchrisumlem1  26052  vmalogdivsum  26102  pntrlog2bndlem5  26144  ostth  26202  tgcgr4  26304  axlowdimlem16  26730  fusgrfisbase  27097  vtxdg0e  27243  rgrusgrprc  27358  wwlksnfi  27671  trlsegvdeglem7  27990  eulerpathpr  28004  0blo  28554  nmlno0lem  28555  omlsilem  29164  pjoc1i  29193  nonbooli  29413  nmlnop0iALT  29757  unopbd  29777  leoprf2  29889  opsqrlem4  29905  opsqrlem5  29906  pjbdlni  29911  pjcmul1i  29963  prsssdm  31168  ordtrestNEW  31172  esumpad  31322  esumpad2  31323  esumcst  31330  esumrnmpt2  31335  sibf0  31600  sitgclcn  31610  sitgclre  31611  eulerpartlemgs2  31646  dstfrvclim1  31743  ballotlemfelz  31756  sgncl  31804  signstfveq0  31855  breprexp  31912  subfacp1lem3  32437  rellysconn  32506  cvmlift2lem9  32566  ordcmp  33803  finxpreclem4  34695  poimirlem16  34955  poimirlem17  34956  voliunnfl  34983  mbfresfi  34985  itg2addnclem2  34991  dvasin  35023  heiborlem4  35134  heiborlem6  35136  wepwsolem  39793  flcidc  39925  iocmbl  39970  arearect  39972  iscard4  40048  briunov2uz  40206  eliunov2uz  40207  frege124d  40269  frege129d  40271  frege92  40464  lhe4.4ex1a  40844  dvconstbi  40849  binomcxplemnn0  40864  binomcxplemnotnn0  40871  infxr  41817  infleinflem2  41821  climneg  42071  cncfiooicc  42355  itgsinexplem1  42415  volioof  42448  stoweidlem36  42497  wallispilem3  42528  fourierdlem93  42660  fouriersw  42692  fouriercn  42693  etransclem16  42711  etransclem33  42728  sge0reuz  42905  nnfoctbdjlem  42913  hoidmvlelem3  43055  dfatafv2ex  43588  sprsymrelfvlem  43826  fmtnofz04prm  43913  nnsum4primeseven  44137  nnsum4primesevenALTV  44138  lincext2  44682  blennn0elnn  44809  itcovalsucov  44889
  Copyright terms: Public domain W3C validator