Theorem eqeltrrid 2838

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

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

This theorem is referenced by:  3eltr3g  2849  dmrnssfld  5969  oprssdm  7590  offval  7681  pwexr  7754  cnvexg  7917  resfunexgALT  7936  abrexexgOLD  7950  abrexex2g  7953  opabex3d  7954  opabex3rd  7955  frxp3  8139  suppssov1  8185  suppssfv  8189  ralxpmap  8892  unfi  9174  pwfir  9178  pwfilem  9179  residfi  9335  imafiALT  9347  abrexfi  9354  ssfii  9416  wdomima2g  9583  unxpwdom2  9585  tskwe  9947  ac10ct  10031  fin23lem28  10337  fin23lem30  10339  axcclem  10454  distrlem4pr  11023  iccshftr  13465  iccshftl  13467  iccdil  13469  icccntr  13471  o1res  15506  exprmfct  16643  infpnlem1  16845  4sqlem13  16892  0ram  16955  ressval3d  17193  ressval3dOLD  17194  ismred2  17549  mreexexlem2d  17591  mreexexlem4d  17593  acsfn1c  17608  acsfn2  17609  ssclem  17768  submacs  18710  symgtset  19269  symgsubmefmndALT  19273  efgrcl  19585  cntrcmnd  19712  cntrabl  19713  dprd2da  19914  srgbinom  20056  irredlmul  20246  lidlrsppropd  20861  chrcl  21084  css1  21249  issubassa  21427  ply1crng  21728  ply1ring  21777  ply1lmod  21781  oftpos  21961  tposmap  21966  0opn  22413  fctop2  22515  difopn  22545  tgrest  22670  ordtbas2  22702  ordtopn3  22707  ordtcld3  22710  t1ficld  22838  resthauslem  22874  kgentopon  23049  txbasex  23077  txcnpi  23119  txdis1cn  23146  pthaus  23149  txkgen  23163  cnmptid  23172  cnmptc  23173  cnmpt1st  23179  cnmpt2nd  23180  cnmpt2c  23181  cnmptkc  23190  txconn  23200  hmeoima  23276  hmeocld  23278  xkohmeo  23326  filufint  23431  fin1aufil  23443  flftg  23507  ptcmplem2  23564  tmdmulg  23603  tmdgsum2  23607  submtmd  23615  symgtgp  23617  ghmcnp  23626  qustgpopn  23631  qustgplem  23632  ust0  23731  nrginvrcn  24216  fsumcn  24393  fsum2cn  24394  expcn  24395  cnheibor  24478  evth2  24483  csscld  24773  clsocv  24774  ovoliun2  25030  volfiniun  25071  dyadmbl  25124  mbfeqalem2  25166  mbfss  25170  ismbf3d  25178  mbfadd  25185  i1f0rn  25206  mbfmul  25251  itg2seq  25267  itg2monolem2  25276  itg2monolem3  25277  itg2mono  25278  itgreval  25321  itgge0  25335  itgss3  25339  iblconst  25342  itgconst  25343  ibladdlem  25344  itgfsum  25351  iblabslem  25352  itgabs  25359  lhop1lem  25537  dvfsumle  25545  dvfsumlem2  25551  ftc1lem4  25563  itgparts  25571  itgsubstlem  25572  itgsubst  25573  plydivlem1  25813  aannenlem1  25848  taylply2  25887  itgulm  25927  cxpcn  26260  resqrtcn  26264  basellem1  26592  mulogsumlem  27041  mulog2sumlem2  27045  selberg2lem  27060  pntrsumo1  27075  addsuniflem  27494  ssltmul1  27612  ssltmul2  27613  precsexlem11  27673  usgrnbcnvfv  28660  ewlksfval  28896  crctcshwlkn0  29113  pjssmii  30972  abrexexd  31784  mptiffisupp  31953  pfxlsw2ccat  32154  cntrcrng  32255  ogrpaddltrbid  32279  ply1degltdimlem  32766  lmatfval  32863  pl1cn  33004  esumcvg  33153  esumcvgsum  33155  sigaval  33178  sigaclfu2  33188  sigapildsys  33229  ldgenpisys  33233  measinb2  33290  braew  33309  unelcarsg  33380  carsgclctunlem2  33387  sibfof  33408  sitgclg  33410  orrvcoel  33533  orrvccel  33534  fsum2dsub  33688  fineqvpow  34165  subfaclefac  34236  cvmsss2  34334  cvmopnlem  34338  satf0suclem  34435  mpstrcl  34601  elmpps  34633  gg-expcn  35233  gg-cmvth  35250  gg-dvfsumle  35251  gg-dvfsumlem2  35252  gg-cxpcn  35253  hmeoclda  35304  bj-1uplex  35975  bj-2uplex  35989  icoreclin  36324  broucube  36608  mblfinlem1  36611  cnambfre  36622  ibladdnclem  36630  iblabsnclem  36637  itgabsnc  36643  ftc1cnnclem  36645  ftc1anclem4  36650  ftc1anclem5  36651  ftc1anclem6  36652  ftc1anclem7  36653  ftc2nc  36656  areacirc  36667  zrdivrng  36907  xrnresex  37362  dalemrot  38614  dalem10  38630  arglem1N  39147  cdlemk36  39870  resopunitintvd  40977  resclunitintvd  40978  lcmineqlem2  40981  mzpconstmpt  41560  mzpresrename  41570  diophrex  41595  0dioph  41598  anrabdioph  41600  orrabdioph  41601  rabren3dioph  41635  dvradcnv2  43188  xpexb  43295  fsumcnf  43787  uzublem  44219  fprodcncf  44695  iblconstmpt  44751  itgiccshift  44775  itgperiod  44776  itgsbtaddcnst  44777  dirkercncflem2  44899  fourierdlem47  44948  saluni  45120  sge0iunmpt  45213  sge0xaddlem2  45229  sge0xadd  45230  hoidmvlelem3  45392  ctvonmbl  45484  vonct  45488  smfaddlem2  45559  smfmullem4  45589  singoutnword  45675  aoprssdm  45989  rngridlmcl  46828  rngqiprngghmlem1  46851  rngqiprnglinlem2  46856  rngqiprngimf1lem  46858  rngqiprng  46860  rngqiprngimf  46861  rngqiprngghm  46863  rngqiprngimf1  46864  rngqiprngimfo  46865  rng2idl1cntr  46869  rngqiprngfulem4  46878  rngqipring1  46880  pzriprnglem6  46889