Theorem eqeltrdi 2870

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

Step	Hyp	Ref	Expression
1		eqeltrdi.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeltrdi.2	. . 3 ⊢ 𝐵 ∈ 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	1, 3	eqeltrd 2862	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837

This theorem is referenced by:  eqeltrrdi  2871  csbexg  5260  unisn2  5262  class2set  5311  snexALT  5340  snexOLD  5399  prexOLD  5400  iotaex  6497  fvrn0  6895  f0cli  7079  funsneqopb  7135  fmptsng  7152  fmptsnd  7153  elimdelov  7492  ovima0  7575  ndmovcl  7581  caovmo  7633  soex  7902  zfrep6OLD  7936  1st2ndb  8010  fprresex  8291  smofvon2  8327  tz7.44-2  8378  oesuclem  8494  omcl  8505  oecl  8506  nnmcl  8582  nnecl  8583  fsetex  8837  fsetexb  8845  ixpexg  8904  resixpfo  8918  xpsnen  9033  ssfi  9141  cnvfi  9144  nnunifi  9235  imafiOLD  9260  prfi  9268  fsuppun  9333  0fsupp  9336  oiexg  9483  hartogslem1  9490  cantnfvalf  9620  rnttrcl  9677  ttrclse  9682  rankdmr1  9759  rankr1c  9779  numwdom  10015  alephon  10025  isfin5  10256  sdom2en01  10259  isf32lem9  10318  hsmexlem9  10382  iundom2g  10497  gchxpidm  10627  r1tskina  10740  tskmcl  10799  recmulnq  10922  recclnq  10924  genpelv  10958  un0mulcl  12515  znegcl  12606  zeo  12659  eqreznegel  12935  xnegcl  13216  xnn0xaddcl  13238  ioorebas  13455  modid0  13907  2txmodxeq0  13944  fzofi  13987  seqexw  14030  expcllem  14085  m1expcl2  14098  faclbnd4lem3  14308  bccl  14335  hasheq0  14376  hashrabrsn  14385  fnfz0hashnn0  14461  fnfzo0hashnn0  14464  wrdnfi  14561  cshwcl  14811  relexpaddg  15066  sgncl  15110  abs00bd  15318  iserge0  15688  sumrblem  15738  fsumcvg  15739  summolem2a  15742  sumss  15751  fsumss  15752  fsumcvg2  15754  sumsplit  15795  binom  15860  bcxmas  15865  geomulcvg  15906  prodrblem  15959  fprodcvg  15960  prodmolem2a  15964  zprod  15967  fprodntriv  15972  prodss  15977  fprodss  15978  binomfallfac  16071  bpoly1  16081  bpoly2  16087  bpoly3  16088  ruclem6  16267  smupf  16512  gcdcl  16540  lcmcl  16635  lcmfcl  16662  2mulprm  16727  pcxnn0cl  16896  pcxcl  16897  pcmptcl  16927  infpnlem2  16947  zgz  16969  4sqlem2  16985  4sqlem19  16999  vdwapval  17009  hashbc0  17041  ramcl2  17052  0ramcl  17059  ramcl  17065  isstruct2  17185  imasval  17541  imasbas  17542  imasds  17543  imasplusg  17547  imasmulr  17548  imasvsca  17550  imasip  17551  imasle  17553  qusaddvallem  17581  qusaddflem  17582  qusaddval  17583  qusaddf  17584  qusmulval  17585  qusmulf  17586  mreexexlem3d  17678  sscpwex  17848  fullresc  17884  estrres  18171  evlfcl  18254  ipopos  18568  gsumress  18716  submnd0  18797  qusgrp2  19100  mulgfval  19111  issubg2  19183  triv1nsgd  19214  0subgALT  19608  torsubg  19894  frgpnabllem1  19913  lt6abl  19935  ablfaclem3  20129  ablfac2  20131  simpgnsgd  20142  qusrng  20226  srgbinomlem3  20274  ringidss  20323  qusring2  20379  isdrngd  20811  isdrngdOLD  20813  mptscmfsupp0  20991  islss3  21023  ellspsn  21067  lspprel  21158  znf1o  21600  frgpcyg  21622  cnmsgnsubg  21626  phlpropd  21704  cssval  21731  iscss  21732  dsmm0cl  21789  uvcvvcl  21836  m1detdiag  22654  m2detleiblem1  22681  pmatcollpw3fi1lem1  22843  indistopon  23058  indiscld  23148  restbas  23215  ordttopon  23250  iocpnfordt  23272  icomnfordt  23273  lecldbas  23276  fiuncmp  23461  cmpfi  23465  conncompid  23488  dissnlocfin  23586  elpt  23629  xkotop  23645  xkouni  23656  xkohaus  23710  xkoptsub  23711  imastopn  23777  filconn  23940  cfinufil  23985  alexsublem  24101  alexsub  24102  alexsubALTlem4  24107  distgp  24156  indistgp  24157  ssblps  24479  ssbl  24480  xmeter  24490  nmoi  24785  nmoeq0  24793  0nghm  24798  idnghm  24800  icccld  24823  iocmnfcld  24825  blssioo  24852  xrtgioo  24864  xrsxmet  24867  icccmp  24883  pcopt  25081  pcopt2  25082  elpi1  25104  cmetcaulem  25347  ishl2  25429  rrxmvallem  25463  ovolcl  25537  ovolunlem1a  25555  ovolunnul  25559  ovoliunnul  25566  ioombl1  25621  icombl  25623  ioombl  25624  iccmbl  25625  iccvolcl  25626  ovolioo  25627  ioovolcl  25629  ioorcl  25636  uniioovol  25638  uniioombllem2a  25641  uniioombllem4  25645  uniioombllem5  25646  vitalilem1  25667  vitalilem5  25671  mbfconstlem  25686  mbfima  25689  mbfid  25694  ismbf2d  25699  mbfss  25705  mbfmulc2lem  25706  i1fd  25740  itg1addlem2  25756  itg1addlem4  25758  itg1addlem5  25759  i1fmulc  25762  itg2l  25788  itg2cl  25791  ibl0  25846  iblrelem  25850  iblpos  25852  iblss2  25865  bddmulibl  25898  bddiblnc  25901  recnperf  25964  ply1remlem  26222  fta1glem1  26225  fta1g  26227  elply  26252  plypf1  26269  coefv0  26305  coemulc  26312  fta1  26369  elqaalem2  26381  aannenlem2  26390  aalioulem3  26395  taylfvallem1  26417  tayl0  26422  ulm0  26451  logtayl  26722  atanrecl  26973  atanbnd  26988  harmonicbnd3  27069  ftalem7  27140  basellem5  27146  ppifi  27167  sqff1o  27243  1sgmprm  27260  logexprlim  27286  dchrelbasd  27300  dchr1re  27324  lgslem4  27361  lgsne0  27396  2sqlem9  27488  2sqlem10  27489  rpvmasumlem  27548  dchrisumlem1  27550  vmalogdivsum  27600  pntrlog2bndlem5  27642  ostth  27700  lrrecse  28032  sltmuls1  28237  sltmuls2  28238  mulsuniflem  28239  noseqex  28379  n0mulscl  28435  n0fincut  28445  eln0s  28451  n0subs  28453  n0zs  28479  expscllem  28520  elz12s  28562  tgcgr4  28697  axlowdimlem16  29155  fusgrfisbase  29526  vtxdg0e  29672  rgrusgrprc  29787  wwlksnfi  30103  trlsegvdeglem7  30425  eulerpathpr  30439  0blo  30992  nmlno0lem  30993  omlsilem  31602  pjoc1i  31631  nonbooli  31851  nmlnop0iALT  32195  unopbd  32215  leoprf2  32327  opsqrlem4  32343  opsqrlem5  32344  pjbdlni  32349  pjcmul1i  32401  mptiffisupp  32892  drngidlhash  33617  evl1deg1  33769  ply1dg1rt  33773  ply1dg3rt0irred  33777  m1pmeq  33778  mplmulmvr  33833  esplyfvaln  33868  vieta  33874  lvecendof1f1o  33927  fldext2rspun  33976  constrabscl  34072  zarcmplem  34175  prsssdm  34211  ordtrestNEW  34215  esumpad  34349  esumpad2  34350  esumcst  34357  esumrnmpt2  34362  sibf0  34628  sitgclcn  34638  sitgclre  34639  eulerpartlemgs2  34674  dstfrvclim1  34772  ballotlemfelz  34785  signstfveq0  34868  breprexp  34924  r1wf  35389  fineqvnttrclselem1  35414  wevgblacfn  35451  subfacp1lem3  35529  rellysconn  35598  cvmlift2lem9  35658  nnuni  36074  ordcmp  36804  bj-snex  37517  finxpreclem4  37885  poimirlem16  38132  poimirlem17  38133  voliunnfl  38160  mbfresfi  38162  itg2addnclem2  38168  dvasin  38200  heiborlem4  38310  heiborlem6  38312  itrere  42924  sn-itrere  43107  sn-retire  43108  wepwsolem  43616  flcidc  43744  iocmbl  43787  arearect  43789  omcl3g  43908  iscard4  44106  briunov2uz  44271  eliunov2uz  44272  frege124d  44334  frege129d  44336  frege92  44528  lhe4.4ex1a  44902  dvconstbi  44907  binomcxplemnn0  44922  binomcxplemnotnn0  44929  infxr  45939  infleinflem2  45943  climneg  46183  cncfiooicc  46465  itgsinexplem1  46525  volioof  46558  stoweidlem36  46607  wallispilem3  46638  fourierdlem93  46770  fouriersw  46802  fouriercn  46803  etransclem16  46821  etransclem33  46838  sge0reuz  47018  nnfoctbdjlem  47026  hoidmvlelem3  47168  sinnpoly  47482  dfatafv2ex  47804  sprsymrelfvlem  48093  fmtnofz04prm  48183  nnsum4primeseven  48419  nnsum4primesevenALTV  48420  gpg3nbgrvtx0  48695  lincext2  49074  blennn0elnn  49196  itcovalsucov  49287  resccat  49692  funcf2lem2  49700  isnatd  49841  swapfelvv  49881  fucoelvv  49938  prcofelvv  49998  termco  50099  prstcprs  50178