Theorem eqeltrrid 2895

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 2807	. 2 ⊢ 𝐴 = 𝐵
3		eqeltrrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrid 2894	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 2770

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

This theorem is referenced by:  3eltr3g  2906  dmrnssfld  5806  oprssdm  7309  offval  7396  pwexr  7467  cnvexg  7611  resfunexgALT  7631  abrexexg  7644  abrexex2g  7647  opabex3d  7648  opabex3rd  7649  suppssov1  7845  suppssfv  7849  ralxpmap  8443  residfi  8789  imafi  8801  abrexfi  8808  ssfii  8867  wdomima2g  9034  unxpwdom2  9036  tskwe  9363  ac10ct  9445  fin23lem28  9751  fin23lem30  9753  axcclem  9868  distrlem4pr  10437  iccshftr  12864  iccshftl  12866  iccdil  12868  icccntr  12870  o1res  14909  exprmfct  16038  infpnlem1  16236  4sqlem13  16283  0ram  16346  ressval3d  16553  ismred2  16866  mreexexlem2d  16908  mreexexlem4d  16910  acsfn1c  16925  acsfn2  16926  ssclem  17081  submacs  17983  symgtset  18519  symgsubmefmndALT  18523  efgrcl  18833  cntrcmnd  18955  cntrabl  18956  dprd2da  19157  srgbinom  19288  irredlmul  19454  lidlrsppropd  19996  chrcl  20218  css1  20379  issubassa  20555  ply1crng  20827  ply1ring  20877  ply1lmod  20881  oftpos  21057  tposmap  21062  0opn  21509  fctop2  21610  difopn  21639  tgrest  21764  ordtbas2  21796  ordtopn3  21801  ordtcld3  21804  t1ficld  21932  resthauslem  21968  kgentopon  22143  txbasex  22171  txcnpi  22213  txdis1cn  22240  pthaus  22243  txkgen  22257  cnmptid  22266  cnmptc  22267  cnmpt1st  22273  cnmpt2nd  22274  cnmpt2c  22275  cnmptkc  22284  txconn  22294  hmeoima  22370  hmeocld  22372  xkohmeo  22420  filufint  22525  fin1aufil  22537  flftg  22601  ptcmplem2  22658  tmdmulg  22697  tmdgsum2  22701  submtmd  22709  symgtgp  22711  ghmcnp  22720  qustgpopn  22725  qustgplem  22726  ust0  22825  nrginvrcn  23298  fsumcn  23475  fsum2cn  23476  expcn  23477  cnheibor  23560  evth2  23565  csscld  23853  clsocv  23854  ovoliun2  24110  volfiniun  24151  dyadmbl  24204  mbfeqalem2  24246  mbfss  24250  ismbf3d  24258  mbfadd  24265  i1f0rn  24286  mbfmul  24330  itg2seq  24346  itg2monolem2  24355  itg2monolem3  24356  itg2mono  24357  itgreval  24400  itgge0  24414  itgss3  24418  iblconst  24421  itgconst  24422  ibladdlem  24423  itgfsum  24430  iblabslem  24431  itgabs  24438  lhop1lem  24616  dvfsumle  24624  dvfsumlem2  24630  ftc1lem4  24642  itgparts  24650  itgsubstlem  24651  itgsubst  24652  plydivlem1  24889  aannenlem1  24924  taylply2  24963  itgulm  25003  cxpcn  25334  resqrtcn  25338  basellem1  25666  mulogsumlem  26115  mulog2sumlem2  26119  selberg2lem  26134  pntrsumo1  26149  usgrnbcnvfv  27155  ewlksfval  27391  crctcshwlkn0  27607  pjssmii  29464  abrexexd  30277  pfxlsw2ccat  30652  cntrcrng  30747  ogrpaddltrbid  30771  lmatfval  31167  pl1cn  31308  esumcvg  31455  esumcvgsum  31457  sigaval  31480  sigaclfu2  31490  sigapildsys  31531  ldgenpisys  31535  measinb2  31592  braew  31611  unelcarsg  31680  carsgclctunlem2  31687  sibfof  31708  sitgclg  31710  orrvcoel  31833  orrvccel  31834  fsum2dsub  31988  subfaclefac  32536  cvmsss2  32634  cvmopnlem  32638  satf0suclem  32735  mpstrcl  32901  elmpps  32933  hmeoclda  33794  bj-1uplex  34444  bj-2uplex  34458  icoreclin  34774  broucube  35091  mblfinlem1  35094  cnambfre  35105  ibladdnclem  35113  iblabsnclem  35120  itgabsnc  35126  ftc1cnnclem  35128  ftc1anclem4  35133  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc2nc  35139  areacirc  35150  zrdivrng  35391  xrnresex  35814  dalemrot  36953  dalem10  36969  arglem1N  37486  cdlemk36  38209  resopunitintvd  39314  resclunitintvd  39315  lcmineqlem2  39318  mzpconstmpt  39681  mzpresrename  39691  diophrex  39716  0dioph  39719  anrabdioph  39721  orrabdioph  39722  rabren3dioph  39756  iunrelexp0  40403  dvradcnv2  41051  xpexb  41158  fsumcnf  41650  uzublem  42067  fprodcncf  42542  iblconstmpt  42598  itgiccshift  42622  itgperiod  42623  itgsbtaddcnst  42624  dirkercncflem2  42746  fourierdlem47  42795  saluni  42966  sge0iunmpt  43057  sge0xaddlem2  43073  sge0xadd  43074  hoidmvlelem3  43236  ctvonmbl  43328  vonct  43332  smfaddlem2  43397  smfmullem4  43426  aoprssdm  43758