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

Theorem eqeltrdi 2848
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 2840 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817
This theorem is referenced by:  eqeltrrdi  2849  csbexg  5235  unisn2  5237  class2set  5277  snexALT  5307  snex  5355  prex  5356  iotaex  6417  fvrn0  6811  f0cli  6983  funsneqopb  7033  fmptsng  7049  fmptsnd  7050  elimdelov  7380  ovima0  7460  ndmovcl  7466  caovmo  7518  soex  7777  zfrep6  7806  1st2ndb  7880  fprresex  8135  wfrlem17OLD  8165  smofvon2  8196  tz7.44-2  8247  oesuclem  8364  omcl  8375  oecl  8376  nnmcl  8452  nnecl  8453  fsetex  8653  fsetexb  8661  ixpexg  8719  resixpfo  8733  en1bOLD  8823  xpsnen  8851  ssfi  8965  imafi  8967  cnvfi  8972  nnunifi  9074  xpfi  9094  fsuppun  9156  0fsupp  9159  oiexg  9303  hartogslem1  9310  cantnfvalf  9432  rnttrcl  9489  ttrclse  9494  rankdmr1  9568  rankr1c  9588  numwdom  9824  alephon  9834  isfin5  10064  sdom2en01  10067  isf32lem9  10126  hsmexlem9  10190  iundom2g  10305  gchxpidm  10434  r1tskina  10547  tskmcl  10606  recmulnq  10729  recclnq  10731  genpelv  10765  un0mulcl  12276  znegcl  12364  zeo  12415  eqreznegel  12683  xnegcl  12956  xnn0xaddcl  12978  ioorebas  13192  modid0  13626  2txmodxeq0  13660  fzofi  13703  seqexw  13746  expcllem  13802  m1expcl2  13813  faclbnd4lem3  14018  bccl  14045  hasheq0  14087  hashrabrsn  14096  fnfz0hashnn0  14169  fnfzo0hashnn0  14172  wrdnfi  14260  ccat2s1p1OLD  14347  cshwcl  14520  relexpaddg  14773  abs00bd  15012  iserge0  15381  sumrblem  15432  fsumcvg  15433  summolem2a  15436  sumss  15445  fsumss  15446  fsumcvg2  15448  sumsplit  15489  binom  15551  bcxmas  15556  geomulcvg  15597  prodrblem  15648  fprodcvg  15649  prodmolem2a  15653  zprod  15656  fprodntriv  15661  prodss  15666  fprodss  15667  binomfallfac  15760  bpoly1  15770  bpoly2  15776  bpoly3  15777  ruclem6  15953  smupf  16194  gcdcl  16222  lcmcl  16315  lcmfcl  16342  2mulprm  16407  pcxnn0cl  16570  pcxcl  16571  pcmptcl  16601  infpnlem2  16621  zgz  16643  4sqlem2  16659  4sqlem19  16673  vdwapval  16683  hashbc0  16715  ramcl2  16726  0ramcl  16733  ramcl  16739  isstruct2  16859  imasval  17231  imasbas  17232  imasds  17233  imasplusg  17237  imasmulr  17238  imasvsca  17240  imasip  17241  imasle  17243  qusaddvallem  17271  qusaddflem  17272  qusaddval  17273  qusaddf  17274  qusmulval  17275  qusmulf  17276  mreexexlem3d  17364  sscpwex  17536  fullresc  17575  estrres  17865  evlfcl  17949  ipopos  18263  gsumress  18375  submnd0  18423  qusgrp2  18702  mulgfval  18711  issubg2  18779  triv1nsgd  18810  torsubg  19464  frgpnabllem1  19483  lt6abl  19505  ablfaclem3  19699  ablfac2  19701  simpgnsgd  19712  srgbinomlem3  19787  ringidss  19825  qusring2  19868  isdrngd  20025  mptscmfsupp0  20197  islss3  20230  lspsnel  20274  lspprel  20365  znf1o  20768  frgpcyg  20790  cnmsgnsubg  20791  phlpropd  20869  cssval  20896  iscss  20897  dsmm0cl  20956  uvcvvcl  21003  m1detdiag  21755  m2detleiblem1  21782  pmatcollpw3fi1lem1  21944  indistopon  22160  indiscld  22251  restbas  22318  ordttopon  22353  iocpnfordt  22375  icomnfordt  22376  lecldbas  22379  fiuncmp  22564  cmpfi  22568  conncompid  22591  dissnlocfin  22689  elpt  22732  xkotop  22748  xkouni  22759  xkohaus  22813  xkoptsub  22814  imastopn  22880  filconn  23043  cfinufil  23088  alexsublem  23204  alexsub  23205  alexsubALTlem4  23210  distgp  23259  indistgp  23260  ssblps  23584  ssbl  23585  xmeter  23595  nmoi  23901  nmoeq0  23909  0nghm  23914  idnghm  23916  icccld  23939  iocmnfcld  23941  blssioo  23967  xrtgioo  23978  xrsxmet  23981  icccmp  23997  pcopt  24194  pcopt2  24195  elpi1  24217  cmetcaulem  24461  ishl2  24543  rrxmvallem  24577  ovolcl  24651  ovolunlem1a  24669  ovolunnul  24673  ovoliunnul  24680  ioombl1  24735  icombl  24737  ioombl  24738  iccmbl  24739  iccvolcl  24740  ovolioo  24741  ioovolcl  24743  ioorcl  24750  uniioovol  24752  uniioombllem2a  24755  uniioombllem4  24759  uniioombllem5  24760  vitalilem1  24781  vitalilem5  24785  mbfconstlem  24800  mbfima  24803  mbfid  24808  ismbf2d  24813  mbfss  24819  mbfmulc2lem  24820  i1fd  24854  itg1addlem2  24870  itg1addlem4  24872  itg1addlem4OLD  24873  itg1addlem5  24874  i1fmulc  24877  itg2l  24903  itg2cl  24906  ibl0  24960  iblrelem  24964  iblpos  24966  iblss2  24979  bddmulibl  25012  bddiblnc  25015  recnperf  25078  ply1remlem  25336  fta1glem1  25339  fta1g  25341  elply  25365  plypf1  25382  coefv0  25418  coemulc  25425  fta1  25477  elqaalem2  25489  aannenlem2  25498  aalioulem3  25503  taylfvallem1  25525  tayl0  25530  ulm0  25559  logtayl  25824  atanrecl  26070  atanbnd  26085  harmonicbnd3  26166  ftalem7  26237  basellem5  26243  ppifi  26264  sqff1o  26340  1sgmprm  26356  logexprlim  26382  dchrelbasd  26396  dchr1re  26420  lgslem4  26457  lgsne0  26492  2sqlem9  26584  2sqlem10  26585  rpvmasumlem  26644  dchrisumlem1  26646  vmalogdivsum  26696  pntrlog2bndlem5  26738  ostth  26796  tgcgr4  26901  axlowdimlem16  27334  fusgrfisbase  27704  vtxdg0e  27850  rgrusgrprc  27965  wwlksnfi  28280  trlsegvdeglem7  28599  eulerpathpr  28613  0blo  29163  nmlno0lem  29164  omlsilem  29773  pjoc1i  29802  nonbooli  30022  nmlnop0iALT  30366  unopbd  30386  leoprf2  30498  opsqrlem4  30514  opsqrlem5  30515  pjbdlni  30520  pjcmul1i  30572  zarcmplem  31840  prsssdm  31876  ordtrestNEW  31880  esumpad  32032  esumpad2  32033  esumcst  32040  esumrnmpt2  32045  sibf0  32310  sitgclcn  32320  sitgclre  32321  eulerpartlemgs2  32356  dstfrvclim1  32453  ballotlemfelz  32466  sgncl  32514  signstfveq0  32565  breprexp  32622  subfacp1lem3  33153  rellysconn  33222  cvmlift2lem9  33282  nnuni  33701  lrrecse  34108  ordcmp  34645  finxpreclem4  35574  poimirlem16  35802  poimirlem17  35803  voliunnfl  35830  mbfresfi  35832  itg2addnclem2  35838  dvasin  35870  heiborlem4  35981  heiborlem6  35983  sn-iotaex  40204  itrere  40443  retire  40444  wepwsolem  40874  flcidc  41006  iocmbl  41051  arearect  41053  iscard4  41147  briunov2uz  41313  eliunov2uz  41314  frege124d  41376  frege129d  41378  frege92  41570  lhe4.4ex1a  41954  dvconstbi  41959  binomcxplemnn0  41974  binomcxplemnotnn0  41981  infxr  42913  infleinflem2  42917  climneg  43158  cncfiooicc  43442  itgsinexplem1  43502  volioof  43535  stoweidlem36  43584  wallispilem3  43615  fourierdlem93  43747  fouriersw  43779  fouriercn  43780  etransclem16  43798  etransclem33  43815  sge0reuz  43992  nnfoctbdjlem  44000  hoidmvlelem3  44142  dfatafv2ex  44716  sprsymrelfvlem  44953  fmtnofz04prm  45040  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  lincext2  45807  blennn0elnn  45934  itcovalsucov  46025  prstcprs  46367  upwordnul  46526
  Copyright terms: Public domain W3C validator