Theorem eqeltrrid 2841

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811

This theorem is referenced by:  3eltr3g  2852  dmrnssfld  5923  oprssdm  7539  offval  7631  pwexr  7710  cnvexg  7866  resfunexgALT  7892  abrexex2g  7908  opabex3d  7909  opabex3rd  7910  frxp3  8093  suppssov1  8139  suppssov2  8140  suppssfv  8144  ralxpmap  8836  unfi  9097  imafi  9217  pwfir  9219  pwfilem  9220  residfi  9240  abrexfi  9254  ssfii  9324  wdomima2g  9493  unxpwdom2  9495  tskwe  9864  ac10ct  9946  fin23lem28  10252  fin23lem30  10254  axcclem  10369  distrlem4pr  10939  iccshftr  13404  iccshftl  13406  iccdil  13408  icccntr  13410  o1res  15485  exprmfct  16633  infpnlem1  16840  4sqlem13  16887  0ram  16950  ressval3d  17175  ismred2  17524  mreexexlem2d  17570  mreexexlem4d  17572  acsfn1c  17587  acsfn2  17588  ssclem  17745  submacs  18754  symgtset  19330  symgsubmefmndALT  19334  efgrcl  19646  cntrcmnd  19773  cntrabl  19774  dprd2da  19975  ogrpaddltrbid  20072  srgbinom  20168  irredlmul  20366  rngridlmcl  21174  lidlrsppropd  21201  rngqiprngghmlem1  21244  rngqiprnglinlem2  21249  rngqiprngimf1lem  21251  rngqiprng  21253  rngqiprngimf  21254  rngqiprngghm  21256  rngqiprngimf1  21257  rngqiprngimfo  21258  rng2idl1cntr  21262  rngqiprngfulem4  21271  rngqipring1  21273  pzriprnglem6  21443  chrcl  21481  css1  21647  issubassa  21824  ply1crng  22141  ply1ring  22190  ply1lmod  22194  oftpos  22398  tposmap  22403  0opn  22850  fctop2  22951  difopn  22980  tgrest  23105  ordtbas2  23137  ordtopn3  23142  ordtcld3  23145  t1ficld  23273  resthauslem  23309  kgentopon  23484  txbasex  23512  txcnpi  23554  txdis1cn  23581  pthaus  23584  txkgen  23598  cnmptid  23607  cnmptc  23608  cnmpt1st  23614  cnmpt2nd  23615  cnmpt2c  23616  cnmptkc  23625  txconn  23635  hmeoima  23711  hmeocld  23713  xkohmeo  23761  filufint  23866  fin1aufil  23878  flftg  23942  ptcmplem2  23999  tmdmulg  24038  tmdgsum2  24042  submtmd  24050  symgtgp  24052  ghmcnp  24061  qustgpopn  24066  qustgplem  24067  ust0  24166  nrginvrcn  24638  fsumcn  24819  fsum2cn  24820  expcn  24821  expcnOLD  24823  cnheibor  24912  evth2  24917  csscld  25207  clsocv  25208  ovoliun2  25465  volfiniun  25506  dyadmbl  25559  mbfeqalem2  25601  mbfss  25605  ismbf3d  25613  mbfadd  25620  i1f0rn  25641  mbfmul  25685  itg2seq  25701  itg2monolem2  25710  itg2monolem3  25711  itg2mono  25712  itgreval  25756  itgge0  25770  itgss3  25774  iblconst  25777  itgconst  25778  ibladdlem  25779  itgfsum  25786  iblabslem  25787  itgabs  25794  cmvth  25953  lhop1lem  25976  dvfsumle  25984  dvfsumleOLD  25985  dvfsumlem2  25991  dvfsumlem2OLD  25992  ftc1lem4  26004  itgparts  26012  itgsubstlem  26013  itgsubst  26014  plydivlem1  26259  aannenlem1  26294  taylply2  26333  taylply2OLD  26334  itgulm  26375  cxpcn  26712  cxpcnOLD  26713  resqrtcn  26717  basellem1  27049  mulogsumlem  27500  mulog2sumlem2  27504  selberg2lem  27519  pntrsumo1  27534  addsuniflem  27999  sltmuls1  28145  sltmuls2  28146  precsexlem11  28215  usgrnbcnvfv  29440  ewlksfval  29677  crctcshwlkn0  29896  pjssmii  31758  rabrexfi  32583  abrexexd  32586  mptiffisupp  32774  pfxlsw2ccat  33034  gsummulsubdishift2s  33156  cntrcrng  33165  dfufd2lem  33632  vietalem  33737  ply1degltdimlem  33781  fldgenfldext  33827  fldextrspunlem2  33836  lmatfval  33973  pl1cn  34114  esumcvg  34245  esumcvgsum  34247  sigaval  34270  sigaclfu2  34280  sigapildsys  34321  ldgenpisys  34325  measinb2  34382  braew  34401  unelcarsg  34471  carsgclctunlem2  34478  sibfof  34499  sitgclg  34501  orrvcoel  34625  orrvccel  34626  fsum2dsub  34766  fineqvpow  35273  subfaclefac  35372  cvmsss2  35470  cvmopnlem  35474  satf0suclem  35571  mpstrcl  35737  elmpps  35769  hmeoclda  36529  bj-1uplex  37211  bj-2uplex  37225  icoreclin  37564  broucube  37857  mblfinlem1  37860  cnambfre  37871  ibladdnclem  37879  iblabsnclem  37886  itgabsnc  37892  ftc1cnnclem  37894  ftc1anclem4  37899  ftc1anclem5  37900  ftc1anclem6  37901  ftc1anclem7  37902  ftc2nc  37905  areacirc  37916  zrdivrng  38156  xrnresex  38627  dalemrot  39939  dalem10  39955  arglem1N  40472  cdlemk36  41195  resopunitintvd  42302  resclunitintvd  42303  lcmineqlem2  42306  aks6d1c7lem1  42456  aks5lem2  42463  mzpconstmpt  43003  mzpresrename  43013  diophrex  43038  0dioph  43041  anrabdioph  43043  orrabdioph  43044  rabren3dioph  43078  dvradcnv2  44609  xpexb  44715  fsumcnf  45287  uzublem  45695  fprodcncf  46165  iblconstmpt  46221  itgiccshift  46245  itgperiod  46246  itgsbtaddcnst  46247  dirkercncflem2  46369  fourierdlem47  46418  saluni  46590  sge0iunmpt  46683  sge0xaddlem2  46699  sge0xadd  46700  hoidmvlelem3  46862  ctvonmbl  46954  vonct  46958  smfaddlem2  47029  smfmullem4  47059  aoprssdm  47469  rescofuf  49359  idfu1stalem  49366  idfu1sta  49367  idfu1a  49368  idfu2nda  49369  oppfuprcl  49470  lmddu  49933  cmddu  49934