Theorem eqeltrrid 2842

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  3eltr3g  2853  dmrnssfld  5931  oprssdm  7549  offval  7641  pwexr  7720  cnvexg  7876  resfunexgALT  7902  abrexex2g  7918  opabex3d  7919  opabex3rd  7920  frxp3  8103  suppssov1  8149  suppssov2  8150  suppssfv  8154  ralxpmap  8846  unfi  9107  imafi  9227  pwfir  9229  pwfilem  9230  residfi  9250  abrexfi  9264  ssfii  9334  wdomima2g  9503  unxpwdom2  9505  tskwe  9874  ac10ct  9956  fin23lem28  10262  fin23lem30  10264  axcclem  10379  distrlem4pr  10949  iccshftr  13414  iccshftl  13416  iccdil  13418  icccntr  13420  o1res  15495  exprmfct  16643  infpnlem1  16850  4sqlem13  16897  0ram  16960  ressval3d  17185  ismred2  17534  mreexexlem2d  17580  mreexexlem4d  17582  acsfn1c  17597  acsfn2  17598  ssclem  17755  submacs  18764  symgtset  19343  symgsubmefmndALT  19347  efgrcl  19659  cntrcmnd  19786  cntrabl  19787  dprd2da  19988  ogrpaddltrbid  20085  srgbinom  20181  irredlmul  20379  rngridlmcl  21187  lidlrsppropd  21214  rngqiprngghmlem1  21257  rngqiprnglinlem2  21262  rngqiprngimf1lem  21264  rngqiprng  21266  rngqiprngimf  21267  rngqiprngghm  21269  rngqiprngimf1  21270  rngqiprngimfo  21271  rng2idl1cntr  21275  rngqiprngfulem4  21284  rngqipring1  21286  pzriprnglem6  21456  chrcl  21494  css1  21660  issubassa  21837  ply1crng  22154  ply1ring  22203  ply1lmod  22207  oftpos  22411  tposmap  22416  0opn  22863  fctop2  22964  difopn  22993  tgrest  23118  ordtbas2  23150  ordtopn3  23155  ordtcld3  23158  t1ficld  23286  resthauslem  23322  kgentopon  23497  txbasex  23525  txcnpi  23567  txdis1cn  23594  pthaus  23597  txkgen  23611  cnmptid  23620  cnmptc  23621  cnmpt1st  23627  cnmpt2nd  23628  cnmpt2c  23629  cnmptkc  23638  txconn  23648  hmeoima  23724  hmeocld  23726  xkohmeo  23774  filufint  23879  fin1aufil  23891  flftg  23955  ptcmplem2  24012  tmdmulg  24051  tmdgsum2  24055  submtmd  24063  symgtgp  24065  ghmcnp  24074  qustgpopn  24079  qustgplem  24080  ust0  24179  nrginvrcn  24651  fsumcn  24832  fsum2cn  24833  expcn  24834  expcnOLD  24836  cnheibor  24925  evth2  24930  csscld  25220  clsocv  25221  ovoliun2  25478  volfiniun  25519  dyadmbl  25572  mbfeqalem2  25614  mbfss  25618  ismbf3d  25626  mbfadd  25633  i1f0rn  25654  mbfmul  25698  itg2seq  25714  itg2monolem2  25723  itg2monolem3  25724  itg2mono  25725  itgreval  25769  itgge0  25783  itgss3  25787  iblconst  25790  itgconst  25791  ibladdlem  25792  itgfsum  25799  iblabslem  25800  itgabs  25807  cmvth  25966  lhop1lem  25989  dvfsumle  25997  dvfsumleOLD  25998  dvfsumlem2  26004  dvfsumlem2OLD  26005  ftc1lem4  26017  itgparts  26025  itgsubstlem  26026  itgsubst  26027  plydivlem1  26272  aannenlem1  26307  taylply2  26346  taylply2OLD  26347  itgulm  26388  cxpcn  26725  cxpcnOLD  26726  resqrtcn  26730  basellem1  27062  mulogsumlem  27513  mulog2sumlem2  27517  selberg2lem  27532  pntrsumo1  27547  addsuniflem  28012  sltmuls1  28158  sltmuls2  28159  precsexlem11  28228  usgrnbcnvfv  29454  ewlksfval  29691  crctcshwlkn0  29910  pjssmii  31773  rabrexfi  32597  abrexexd  32600  mptiffisupp  32787  pfxlsw2ccat  33047  gsummulsubdishift2s  33169  cntrcrng  33179  dfufd2lem  33646  vietalem  33760  ply1degltdimlem  33804  fldgenfldext  33850  fldextrspunlem2  33859  lmatfval  33996  pl1cn  34137  esumcvg  34268  esumcvgsum  34270  sigaval  34293  sigaclfu2  34303  sigapildsys  34344  ldgenpisys  34348  measinb2  34405  braew  34424  unelcarsg  34494  carsgclctunlem2  34501  sibfof  34522  sitgclg  34524  orrvcoel  34648  orrvccel  34649  fsum2dsub  34789  fineqvpow  35297  subfaclefac  35396  cvmsss2  35494  cvmopnlem  35498  satf0suclem  35595  mpstrcl  35761  elmpps  35793  hmeoclda  36553  bj-1uplex  37260  bj-2uplex  37274  icoreclin  37616  broucube  37909  mblfinlem1  37912  cnambfre  37923  ibladdnclem  37931  iblabsnclem  37938  itgabsnc  37944  ftc1cnnclem  37946  ftc1anclem4  37951  ftc1anclem5  37952  ftc1anclem6  37953  ftc1anclem7  37954  ftc2nc  37957  areacirc  37968  zrdivrng  38208  xrnresex  38684  dalemrot  40037  dalem10  40053  arglem1N  40570  cdlemk36  41293  resopunitintvd  42400  resclunitintvd  42401  lcmineqlem2  42404  aks6d1c7lem1  42554  aks5lem2  42561  mzpconstmpt  43101  mzpresrename  43111  diophrex  43136  0dioph  43139  anrabdioph  43141  orrabdioph  43142  rabren3dioph  43176  dvradcnv2  44707  xpexb  44813  fsumcnf  45385  uzublem  45792  fprodcncf  46262  iblconstmpt  46318  itgiccshift  46342  itgperiod  46343  itgsbtaddcnst  46344  dirkercncflem2  46466  fourierdlem47  46515  saluni  46687  sge0iunmpt  46780  sge0xaddlem2  46796  sge0xadd  46797  hoicvr  46910  hoidmvlelem3  46959  ctvonmbl  47051  vonct  47055  smfaddlem2  47126  smfmullem4  47156  aoprssdm  47566  rescofuf  49456  idfu1stalem  49463  idfu1sta  49464  idfu1a  49465  idfu2nda  49466  oppfuprcl  49567  lmddu  50030  cmddu  50031