Theorem eqeltrrid 2846

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 2845	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 2708

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

This theorem is referenced by:  3eltr3g  2857  dmrnssfld  5984  oprssdm  7614  offval  7706  pwexr  7785  cnvexg  7946  resfunexgALT  7972  abrexexgOLD  7986  abrexex2g  7989  opabex3d  7990  opabex3rd  7991  frxp3  8176  suppssov1  8222  suppssov2  8223  suppssfv  8227  ralxpmap  8936  unfi  9211  imafi  9353  pwfir  9355  pwfilem  9356  residfi  9378  abrexfi  9392  ssfii  9459  wdomima2g  9626  unxpwdom2  9628  tskwe  9990  ac10ct  10074  fin23lem28  10380  fin23lem30  10382  axcclem  10497  distrlem4pr  11066  iccshftr  13526  iccshftl  13528  iccdil  13530  icccntr  13532  o1res  15596  exprmfct  16741  infpnlem1  16948  4sqlem13  16995  0ram  17058  ressval3d  17292  ismred2  17646  mreexexlem2d  17688  mreexexlem4d  17690  acsfn1c  17705  acsfn2  17706  ssclem  17863  submacs  18840  symgtset  19417  symgsubmefmndALT  19421  efgrcl  19733  cntrcmnd  19860  cntrabl  19861  dprd2da  20062  srgbinom  20228  irredlmul  20428  rngridlmcl  21227  lidlrsppropd  21254  rngqiprngghmlem1  21297  rngqiprnglinlem2  21302  rngqiprngimf1lem  21304  rngqiprng  21306  rngqiprngimf  21307  rngqiprngghm  21309  rngqiprngimf1  21310  rngqiprngimfo  21311  rng2idl1cntr  21315  rngqiprngfulem4  21324  rngqipring1  21326  pzriprnglem6  21497  chrcl  21539  css1  21708  issubassa  21887  ply1crng  22200  ply1ring  22249  ply1lmod  22253  oftpos  22458  tposmap  22463  0opn  22910  fctop2  23012  difopn  23042  tgrest  23167  ordtbas2  23199  ordtopn3  23204  ordtcld3  23207  t1ficld  23335  resthauslem  23371  kgentopon  23546  txbasex  23574  txcnpi  23616  txdis1cn  23643  pthaus  23646  txkgen  23660  cnmptid  23669  cnmptc  23670  cnmpt1st  23676  cnmpt2nd  23677  cnmpt2c  23678  cnmptkc  23687  txconn  23697  hmeoima  23773  hmeocld  23775  xkohmeo  23823  filufint  23928  fin1aufil  23940  flftg  24004  ptcmplem2  24061  tmdmulg  24100  tmdgsum2  24104  submtmd  24112  symgtgp  24114  ghmcnp  24123  qustgpopn  24128  qustgplem  24129  ust0  24228  nrginvrcn  24713  fsumcn  24894  fsum2cn  24895  expcn  24896  expcnOLD  24898  cnheibor  24987  evth2  24992  csscld  25283  clsocv  25284  ovoliun2  25541  volfiniun  25582  dyadmbl  25635  mbfeqalem2  25677  mbfss  25681  ismbf3d  25689  mbfadd  25696  i1f0rn  25717  mbfmul  25761  itg2seq  25777  itg2monolem2  25786  itg2monolem3  25787  itg2mono  25788  itgreval  25832  itgge0  25846  itgss3  25850  iblconst  25853  itgconst  25854  ibladdlem  25855  itgfsum  25862  iblabslem  25863  itgabs  25870  cmvth  26029  lhop1lem  26052  dvfsumle  26060  dvfsumleOLD  26061  dvfsumlem2  26067  dvfsumlem2OLD  26068  ftc1lem4  26080  itgparts  26088  itgsubstlem  26089  itgsubst  26090  plydivlem1  26335  aannenlem1  26370  taylply2  26409  taylply2OLD  26410  itgulm  26451  cxpcn  26787  cxpcnOLD  26788  resqrtcn  26792  basellem1  27124  mulogsumlem  27575  mulog2sumlem2  27579  selberg2lem  27594  pntrsumo1  27609  addsuniflem  28034  ssltmul1  28173  ssltmul2  28174  precsexlem11  28241  usgrnbcnvfv  29382  ewlksfval  29619  crctcshwlkn0  29841  pjssmii  31700  rabrexfi  32525  abrexexd  32528  mptiffisupp  32702  pfxlsw2ccat  32935  cntrcrng  33073  ogrpaddltrbid  33097  dfufd2lem  33577  ply1degltdimlem  33673  fldgenfldext  33718  fldextrspunlem2  33727  lmatfval  33813  pl1cn  33954  esumcvg  34087  esumcvgsum  34089  sigaval  34112  sigaclfu2  34122  sigapildsys  34163  ldgenpisys  34167  measinb2  34224  braew  34243  unelcarsg  34314  carsgclctunlem2  34321  sibfof  34342  sitgclg  34344  orrvcoel  34468  orrvccel  34469  fsum2dsub  34622  fineqvpow  35110  subfaclefac  35181  cvmsss2  35279  cvmopnlem  35283  satf0suclem  35380  mpstrcl  35546  elmpps  35578  hmeoclda  36334  bj-1uplex  37009  bj-2uplex  37023  icoreclin  37358  broucube  37661  mblfinlem1  37664  cnambfre  37675  ibladdnclem  37683  iblabsnclem  37690  itgabsnc  37696  ftc1cnnclem  37698  ftc1anclem4  37703  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc2nc  37709  areacirc  37720  zrdivrng  37960  xrnresex  38407  dalemrot  39659  dalem10  39675  arglem1N  40192  cdlemk36  40915  resopunitintvd  42027  resclunitintvd  42028  lcmineqlem2  42031  aks6d1c7lem1  42181  aks5lem2  42188  mzpconstmpt  42751  mzpresrename  42761  diophrex  42786  0dioph  42789  anrabdioph  42791  orrabdioph  42792  rabren3dioph  42826  dvradcnv2  44366  xpexb  44473  fsumcnf  45026  uzublem  45441  fprodcncf  45915  iblconstmpt  45971  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  dirkercncflem2  46119  fourierdlem47  46168  saluni  46340  sge0iunmpt  46433  sge0xaddlem2  46449  sge0xadd  46450  hoidmvlelem3  46612  ctvonmbl  46704  vonct  46708  smfaddlem2  46779  smfmullem4  46809  singoutnword  46897  aoprssdm  47214  rescofuf  48922