Theorem eqeltrrid 2845

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731  df-clel 2817

This theorem is referenced by:  3eltr3g  2856  dmrnssfld  5876  oprssdm  7444  offval  7533  pwexr  7606  cnvexg  7758  resfunexgALT  7777  abrexexg  7790  abrexex2g  7793  opabex3d  7794  opabex3rd  7795  suppssov1  7998  suppssfv  8002  ralxpmap  8658  unfi  8920  pwfir  8924  pwfilem  8925  residfi  9061  imafiALT  9073  abrexfi  9080  ssfii  9139  wdomima2g  9306  unxpwdom2  9308  tskwe  9692  ac10ct  9774  fin23lem28  10080  fin23lem30  10082  axcclem  10197  distrlem4pr  10766  iccshftr  13200  iccshftl  13202  iccdil  13204  icccntr  13206  o1res  15250  exprmfct  16390  infpnlem1  16592  4sqlem13  16639  0ram  16702  ressval3d  16937  ressval3dOLD  16938  ismred2  17293  mreexexlem2d  17335  mreexexlem4d  17337  acsfn1c  17352  acsfn2  17353  ssclem  17512  submacs  18446  symgtset  18988  symgsubmefmndALT  18992  efgrcl  19302  cntrcmnd  19424  cntrabl  19425  dprd2da  19626  srgbinom  19762  irredlmul  19931  lidlrsppropd  20482  chrcl  20711  css1  20876  issubassa  21054  ply1crng  21350  ply1ring  21400  ply1lmod  21404  oftpos  21582  tposmap  21587  0opn  22034  fctop2  22136  difopn  22166  tgrest  22291  ordtbas2  22323  ordtopn3  22328  ordtcld3  22331  t1ficld  22459  resthauslem  22495  kgentopon  22670  txbasex  22698  txcnpi  22740  txdis1cn  22767  pthaus  22770  txkgen  22784  cnmptid  22793  cnmptc  22794  cnmpt1st  22800  cnmpt2nd  22801  cnmpt2c  22802  cnmptkc  22811  txconn  22821  hmeoima  22897  hmeocld  22899  xkohmeo  22947  filufint  23052  fin1aufil  23064  flftg  23128  ptcmplem2  23185  tmdmulg  23224  tmdgsum2  23228  submtmd  23236  symgtgp  23238  ghmcnp  23247  qustgpopn  23252  qustgplem  23253  ust0  23352  nrginvrcn  23837  fsumcn  24014  fsum2cn  24015  expcn  24016  cnheibor  24099  evth2  24104  csscld  24394  clsocv  24395  ovoliun2  24651  volfiniun  24692  dyadmbl  24745  mbfeqalem2  24787  mbfss  24791  ismbf3d  24799  mbfadd  24806  i1f0rn  24827  mbfmul  24872  itg2seq  24888  itg2monolem2  24897  itg2monolem3  24898  itg2mono  24899  itgreval  24942  itgge0  24956  itgss3  24960  iblconst  24963  itgconst  24964  ibladdlem  24965  itgfsum  24972  iblabslem  24973  itgabs  24980  lhop1lem  25158  dvfsumle  25166  dvfsumlem2  25172  ftc1lem4  25184  itgparts  25192  itgsubstlem  25193  itgsubst  25194  plydivlem1  25434  aannenlem1  25469  taylply2  25508  itgulm  25548  cxpcn  25879  resqrtcn  25883  basellem1  26211  mulogsumlem  26660  mulog2sumlem2  26664  selberg2lem  26679  pntrsumo1  26694  usgrnbcnvfv  27713  ewlksfval  27949  crctcshwlkn0  28165  pjssmii  30022  abrexexd  30833  pfxlsw2ccat  31203  cntrcrng  31301  ogrpaddltrbid  31325  lmatfval  31743  pl1cn  31884  esumcvg  32033  esumcvgsum  32035  sigaval  32058  sigaclfu2  32068  sigapildsys  32109  ldgenpisys  32113  measinb2  32170  braew  32189  unelcarsg  32258  carsgclctunlem2  32265  sibfof  32286  sitgclg  32288  orrvcoel  32411  orrvccel  32412  fsum2dsub  32566  fineqvpow  33044  subfaclefac  33117  cvmsss2  33215  cvmopnlem  33219  satf0suclem  33316  mpstrcl  33482  elmpps  33514  hmeoclda  34501  bj-1uplex  35177  bj-2uplex  35191  icoreclin  35507  broucube  35790  mblfinlem1  35793  cnambfre  35804  ibladdnclem  35812  iblabsnclem  35819  itgabsnc  35825  ftc1cnnclem  35827  ftc1anclem4  35832  ftc1anclem5  35833  ftc1anclem6  35834  ftc1anclem7  35835  ftc2nc  35838  areacirc  35849  zrdivrng  36090  xrnresex  36511  dalemrot  37650  dalem10  37666  arglem1N  38183  cdlemk36  38906  resopunitintvd  40014  resclunitintvd  40015  lcmineqlem2  40018  mzpconstmpt  40542  mzpresrename  40552  diophrex  40577  0dioph  40580  anrabdioph  40582  orrabdioph  40583  rabren3dioph  40617  iunrelexp0  41263  dvradcnv2  41918  xpexb  42025  fsumcnf  42517  uzublem  42924  fprodcncf  43395  iblconstmpt  43451  itgiccshift  43475  itgperiod  43476  itgsbtaddcnst  43477  dirkercncflem2  43599  fourierdlem47  43648  saluni  43819  sge0iunmpt  43910  sge0xaddlem2  43926  sge0xadd  43927  hoidmvlelem3  44089  ctvonmbl  44181  vonct  44185  smfaddlem2  44250  smfmullem4  44279  aoprssdm  44645