Theorem eqeltrrid 2857

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eqeltrrid.1	⊢ 𝐵 = 𝐴
eqeltrrid.2	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
eqeltrrid	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrrid

Step	Hyp	Ref	Expression
1		eqeltrrid.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2767	. 2 ⊢ 𝐴 = 𝐵
3		eqeltrrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrid 2856	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-clel 2830

This theorem is referenced by:  3eltr3g  2868  dmrnssfld  5816  oprssdm  7331  offval  7419  pwexr  7492  cnvexg  7640  resfunexgALT  7659  abrexexg  7672  abrexex2g  7675  opabex3d  7676  opabex3rd  7677  suppssov1  7878  suppssfv  7882  ralxpmap  8491  unfi  8754  pwfir  8757  pwfilem  8758  residfi  8851  imafiOLD  8863  abrexfi  8870  ssfii  8929  wdomima2g  9096  unxpwdom2  9098  tskwe  9425  ac10ct  9507  fin23lem28  9813  fin23lem30  9815  axcclem  9930  distrlem4pr  10499  iccshftr  12931  iccshftl  12933  iccdil  12935  icccntr  12937  o1res  14978  exprmfct  16114  infpnlem1  16315  4sqlem13  16362  0ram  16425  ressval3d  16633  ismred2  16946  mreexexlem2d  16988  mreexexlem4d  16990  acsfn1c  17005  acsfn2  17006  ssclem  17162  submacs  18071  symgtset  18608  symgsubmefmndALT  18612  efgrcl  18922  cntrcmnd  19044  cntrabl  19045  dprd2da  19246  srgbinom  19377  irredlmul  19543  lidlrsppropd  20085  chrcl  20308  css1  20469  issubassa  20645  ply1crng  20936  ply1ring  20986  ply1lmod  20990  oftpos  21166  tposmap  21171  0opn  21618  fctop2  21719  difopn  21748  tgrest  21873  ordtbas2  21905  ordtopn3  21910  ordtcld3  21913  t1ficld  22041  resthauslem  22077  kgentopon  22252  txbasex  22280  txcnpi  22322  txdis1cn  22349  pthaus  22352  txkgen  22366  cnmptid  22375  cnmptc  22376  cnmpt1st  22382  cnmpt2nd  22383  cnmpt2c  22384  cnmptkc  22393  txconn  22403  hmeoima  22479  hmeocld  22481  xkohmeo  22529  filufint  22634  fin1aufil  22646  flftg  22710  ptcmplem2  22767  tmdmulg  22806  tmdgsum2  22810  submtmd  22818  symgtgp  22820  ghmcnp  22829  qustgpopn  22834  qustgplem  22835  ust0  22934  nrginvrcn  23408  fsumcn  23585  fsum2cn  23586  expcn  23587  cnheibor  23670  evth2  23675  csscld  23963  clsocv  23964  ovoliun2  24220  volfiniun  24261  dyadmbl  24314  mbfeqalem2  24356  mbfss  24360  ismbf3d  24368  mbfadd  24375  i1f0rn  24396  mbfmul  24440  itg2seq  24456  itg2monolem2  24465  itg2monolem3  24466  itg2mono  24467  itgreval  24510  itgge0  24524  itgss3  24528  iblconst  24531  itgconst  24532  ibladdlem  24533  itgfsum  24540  iblabslem  24541  itgabs  24548  lhop1lem  24726  dvfsumle  24734  dvfsumlem2  24740  ftc1lem4  24752  itgparts  24760  itgsubstlem  24761  itgsubst  24762  plydivlem1  25002  aannenlem1  25037  taylply2  25076  itgulm  25116  cxpcn  25447  resqrtcn  25451  basellem1  25779  mulogsumlem  26228  mulog2sumlem2  26232  selberg2lem  26247  pntrsumo1  26262  usgrnbcnvfv  27268  ewlksfval  27504  crctcshwlkn0  27720  pjssmii  29577  abrexexd  30390  pfxlsw2ccat  30761  cntrcrng  30861  ogrpaddltrbid  30885  lmatfval  31298  pl1cn  31439  esumcvg  31586  esumcvgsum  31588  sigaval  31611  sigaclfu2  31621  sigapildsys  31662  ldgenpisys  31666  measinb2  31723  braew  31742  unelcarsg  31811  carsgclctunlem2  31818  sibfof  31839  sitgclg  31841  orrvcoel  31964  orrvccel  31965  fsum2dsub  32119  subfaclefac  32667  cvmsss2  32765  cvmopnlem  32769  satf0suclem  32866  mpstrcl  33032  elmpps  33064  hmeoclda  34106  bj-1uplex  34760  bj-2uplex  34774  icoreclin  35089  broucube  35406  mblfinlem1  35409  cnambfre  35420  ibladdnclem  35428  iblabsnclem  35435  itgabsnc  35441  ftc1cnnclem  35443  ftc1anclem4  35448  ftc1anclem5  35449  ftc1anclem6  35450  ftc1anclem7  35451  ftc2nc  35454  areacirc  35465  zrdivrng  35706  xrnresex  36129  dalemrot  37268  dalem10  37284  arglem1N  37801  cdlemk36  38524  resopunitintvd  39628  resclunitintvd  39629  lcmineqlem2  39632  mzpconstmpt  40099  mzpresrename  40109  diophrex  40134  0dioph  40137  anrabdioph  40139  orrabdioph  40140  rabren3dioph  40174  iunrelexp0  40821  dvradcnv2  41469  xpexb  41576  fsumcnf  42068  uzublem  42478  fprodcncf  42953  iblconstmpt  43009  itgiccshift  43033  itgperiod  43034  itgsbtaddcnst  43035  dirkercncflem2  43157  fourierdlem47  43206  saluni  43377  sge0iunmpt  43468  sge0xaddlem2  43484  sge0xadd  43485  hoidmvlelem3  43647  ctvonmbl  43739  vonct  43743  smfaddlem2  43808  smfmullem4  43837  aoprssdm  44185