Theorem eqeltrrid 2837

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809

This theorem is referenced by:  3eltr3g  2848  dmrnssfld  5961  oprssdm  7571  offval  7662  pwexr  7735  cnvexg  7897  resfunexgALT  7916  abrexexgOLD  7930  abrexex2g  7933  opabex3d  7934  opabex3rd  7935  frxp3  8119  suppssov1  8165  suppssfv  8169  ralxpmap  8873  unfi  9155  pwfir  9159  pwfilem  9160  residfi  9316  imafiALT  9328  abrexfi  9335  ssfii  9396  wdomima2g  9563  unxpwdom2  9565  tskwe  9927  ac10ct  10011  fin23lem28  10317  fin23lem30  10319  axcclem  10434  distrlem4pr  11003  iccshftr  13445  iccshftl  13447  iccdil  13449  icccntr  13451  o1res  15486  exprmfct  16623  infpnlem1  16825  4sqlem13  16872  0ram  16935  ressval3d  17173  ressval3dOLD  17174  ismred2  17529  mreexexlem2d  17571  mreexexlem4d  17573  acsfn1c  17588  acsfn2  17589  ssclem  17748  submacs  18683  symgtset  19231  symgsubmefmndALT  19235  efgrcl  19547  cntrcmnd  19670  cntrabl  19671  dprd2da  19871  srgbinom  20012  irredlmul  20192  lidlrsppropd  20801  chrcl  21011  css1  21176  issubassa  21354  ply1crng  21651  ply1ring  21701  ply1lmod  21705  oftpos  21883  tposmap  21888  0opn  22335  fctop2  22437  difopn  22467  tgrest  22592  ordtbas2  22624  ordtopn3  22629  ordtcld3  22632  t1ficld  22760  resthauslem  22796  kgentopon  22971  txbasex  22999  txcnpi  23041  txdis1cn  23068  pthaus  23071  txkgen  23085  cnmptid  23094  cnmptc  23095  cnmpt1st  23101  cnmpt2nd  23102  cnmpt2c  23103  cnmptkc  23112  txconn  23122  hmeoima  23198  hmeocld  23200  xkohmeo  23248  filufint  23353  fin1aufil  23365  flftg  23429  ptcmplem2  23486  tmdmulg  23525  tmdgsum2  23529  submtmd  23537  symgtgp  23539  ghmcnp  23548  qustgpopn  23553  qustgplem  23554  ust0  23653  nrginvrcn  24138  fsumcn  24315  fsum2cn  24316  expcn  24317  cnheibor  24400  evth2  24405  csscld  24695  clsocv  24696  ovoliun2  24952  volfiniun  24993  dyadmbl  25046  mbfeqalem2  25088  mbfss  25092  ismbf3d  25100  mbfadd  25107  i1f0rn  25128  mbfmul  25173  itg2seq  25189  itg2monolem2  25198  itg2monolem3  25199  itg2mono  25200  itgreval  25243  itgge0  25257  itgss3  25261  iblconst  25264  itgconst  25265  ibladdlem  25266  itgfsum  25273  iblabslem  25274  itgabs  25281  lhop1lem  25459  dvfsumle  25467  dvfsumlem2  25473  ftc1lem4  25485  itgparts  25493  itgsubstlem  25494  itgsubst  25495  plydivlem1  25735  aannenlem1  25770  taylply2  25809  itgulm  25849  cxpcn  26180  resqrtcn  26184  basellem1  26512  mulogsumlem  26961  mulog2sumlem2  26965  selberg2lem  26980  pntrsumo1  26995  addsuniflem  27400  ssltmul1  27514  ssltmul2  27515  usgrnbcnvfv  28487  ewlksfval  28723  crctcshwlkn0  28940  pjssmii  30797  abrexexd  31610  mptiffisupp  31786  pfxlsw2ccat  31987  cntrcrng  32085  ogrpaddltrbid  32109  ply1degltdimlem  32543  lmatfval  32623  pl1cn  32764  esumcvg  32913  esumcvgsum  32915  sigaval  32938  sigaclfu2  32948  sigapildsys  32989  ldgenpisys  32993  measinb2  33050  braew  33069  unelcarsg  33140  carsgclctunlem2  33147  sibfof  33168  sitgclg  33170  orrvcoel  33293  orrvccel  33294  fsum2dsub  33448  fineqvpow  33925  subfaclefac  33996  cvmsss2  34094  cvmopnlem  34098  satf0suclem  34195  mpstrcl  34361  elmpps  34393  hmeoclda  35020  bj-1uplex  35691  bj-2uplex  35705  icoreclin  36040  broucube  36324  mblfinlem1  36327  cnambfre  36338  ibladdnclem  36346  iblabsnclem  36353  itgabsnc  36359  ftc1cnnclem  36361  ftc1anclem4  36366  ftc1anclem5  36367  ftc1anclem6  36368  ftc1anclem7  36369  ftc2nc  36372  areacirc  36383  zrdivrng  36624  xrnresex  37079  dalemrot  38331  dalem10  38347  arglem1N  38864  cdlemk36  39587  resopunitintvd  40694  resclunitintvd  40695  lcmineqlem2  40698  mzpconstmpt  41247  mzpresrename  41257  diophrex  41282  0dioph  41285  anrabdioph  41287  orrabdioph  41288  rabren3dioph  41322  dvradcnv2  42875  xpexb  42982  fsumcnf  43474  uzublem  43911  fprodcncf  44387  iblconstmpt  44443  itgiccshift  44467  itgperiod  44468  itgsbtaddcnst  44469  dirkercncflem2  44591  fourierdlem47  44640  saluni  44812  sge0iunmpt  44905  sge0xaddlem2  44921  sge0xadd  44922  hoidmvlelem3  45084  ctvonmbl  45176  vonct  45180  smfaddlem2  45251  smfmullem4  45281  singoutnword  45367  aoprssdm  45680