Theorem eqeltrrid 2839

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809

This theorem is referenced by:  3eltr3g  2850  dmrnssfld  5953  oprssdm  7586  offval  7678  pwexr  7757  cnvexg  7918  resfunexgALT  7944  abrexexgOLD  7958  abrexex2g  7961  opabex3d  7962  opabex3rd  7963  frxp3  8148  suppssov1  8194  suppssov2  8195  suppssfv  8199  ralxpmap  8908  unfi  9183  imafi  9323  pwfir  9325  pwfilem  9326  residfi  9348  abrexfi  9362  ssfii  9429  wdomima2g  9598  unxpwdom2  9600  tskwe  9962  ac10ct  10046  fin23lem28  10352  fin23lem30  10354  axcclem  10469  distrlem4pr  11038  iccshftr  13501  iccshftl  13503  iccdil  13505  icccntr  13507  o1res  15574  exprmfct  16721  infpnlem1  16928  4sqlem13  16975  0ram  17038  ressval3d  17265  ismred2  17613  mreexexlem2d  17655  mreexexlem4d  17657  acsfn1c  17672  acsfn2  17673  ssclem  17830  submacs  18803  symgtset  19378  symgsubmefmndALT  19382  efgrcl  19694  cntrcmnd  19821  cntrabl  19822  dprd2da  20023  srgbinom  20189  irredlmul  20386  rngridlmcl  21176  lidlrsppropd  21203  rngqiprngghmlem1  21246  rngqiprnglinlem2  21251  rngqiprngimf1lem  21253  rngqiprng  21255  rngqiprngimf  21256  rngqiprngghm  21258  rngqiprngimf1  21259  rngqiprngimfo  21260  rng2idl1cntr  21264  rngqiprngfulem4  21273  rngqipring1  21275  pzriprnglem6  21445  chrcl  21483  css1  21648  issubassa  21825  ply1crng  22132  ply1ring  22181  ply1lmod  22185  oftpos  22388  tposmap  22393  0opn  22840  fctop2  22941  difopn  22970  tgrest  23095  ordtbas2  23127  ordtopn3  23132  ordtcld3  23135  t1ficld  23263  resthauslem  23299  kgentopon  23474  txbasex  23502  txcnpi  23544  txdis1cn  23571  pthaus  23574  txkgen  23588  cnmptid  23597  cnmptc  23598  cnmpt1st  23604  cnmpt2nd  23605  cnmpt2c  23606  cnmptkc  23615  txconn  23625  hmeoima  23701  hmeocld  23703  xkohmeo  23751  filufint  23856  fin1aufil  23868  flftg  23932  ptcmplem2  23989  tmdmulg  24028  tmdgsum2  24032  submtmd  24040  symgtgp  24042  ghmcnp  24051  qustgpopn  24056  qustgplem  24057  ust0  24156  nrginvrcn  24629  fsumcn  24810  fsum2cn  24811  expcn  24812  expcnOLD  24814  cnheibor  24903  evth2  24908  csscld  25199  clsocv  25200  ovoliun2  25457  volfiniun  25498  dyadmbl  25551  mbfeqalem2  25593  mbfss  25597  ismbf3d  25605  mbfadd  25612  i1f0rn  25633  mbfmul  25677  itg2seq  25693  itg2monolem2  25702  itg2monolem3  25703  itg2mono  25704  itgreval  25748  itgge0  25762  itgss3  25766  iblconst  25769  itgconst  25770  ibladdlem  25771  itgfsum  25778  iblabslem  25779  itgabs  25786  cmvth  25945  lhop1lem  25968  dvfsumle  25976  dvfsumleOLD  25977  dvfsumlem2  25983  dvfsumlem2OLD  25984  ftc1lem4  25996  itgparts  26004  itgsubstlem  26005  itgsubst  26006  plydivlem1  26251  aannenlem1  26286  taylply2  26325  taylply2OLD  26326  itgulm  26367  cxpcn  26704  cxpcnOLD  26705  resqrtcn  26709  basellem1  27041  mulogsumlem  27492  mulog2sumlem2  27496  selberg2lem  27511  pntrsumo1  27526  addsuniflem  27951  ssltmul1  28090  ssltmul2  28091  precsexlem11  28158  usgrnbcnvfv  29290  ewlksfval  29527  crctcshwlkn0  29749  pjssmii  31608  rabrexfi  32433  abrexexd  32436  mptiffisupp  32616  pfxlsw2ccat  32872  cntrcrng  33010  ogrpaddltrbid  33034  dfufd2lem  33510  ply1degltdimlem  33608  fldgenfldext  33655  fldextrspunlem2  33664  lmatfval  33791  pl1cn  33932  esumcvg  34063  esumcvgsum  34065  sigaval  34088  sigaclfu2  34098  sigapildsys  34139  ldgenpisys  34143  measinb2  34200  braew  34219  unelcarsg  34290  carsgclctunlem2  34297  sibfof  34318  sitgclg  34320  orrvcoel  34444  orrvccel  34445  fsum2dsub  34585  fineqvpow  35073  subfaclefac  35144  cvmsss2  35242  cvmopnlem  35246  satf0suclem  35343  mpstrcl  35509  elmpps  35541  hmeoclda  36297  bj-1uplex  36972  bj-2uplex  36986  icoreclin  37321  broucube  37624  mblfinlem1  37627  cnambfre  37638  ibladdnclem  37646  iblabsnclem  37653  itgabsnc  37659  ftc1cnnclem  37661  ftc1anclem4  37666  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc2nc  37672  areacirc  37683  zrdivrng  37923  xrnresex  38370  dalemrot  39622  dalem10  39638  arglem1N  40155  cdlemk36  40878  resopunitintvd  41985  resclunitintvd  41986  lcmineqlem2  41989  aks6d1c7lem1  42139  aks5lem2  42146  mzpconstmpt  42710  mzpresrename  42720  diophrex  42745  0dioph  42748  anrabdioph  42750  orrabdioph  42751  rabren3dioph  42785  dvradcnv2  44319  xpexb  44426  fsumcnf  44993  uzublem  45405  fprodcncf  45877  iblconstmpt  45933  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  dirkercncflem2  46081  fourierdlem47  46130  saluni  46302  sge0iunmpt  46395  sge0xaddlem2  46411  sge0xadd  46412  hoidmvlelem3  46574  ctvonmbl  46666  vonct  46670  smfaddlem2  46741  smfmullem4  46771  singoutnword  46859  aoprssdm  47179  rescofuf  49004  idfu1stalem  49007  idfu1sta  49008  idfu1a  49009  idfu2nda  49010  2oppffunc  49037  oppfuprcl  49085