Theorem eqeltrrid 2833

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3eltr3g  2844  dmrnssfld  5915  oprssdm  7530  offval  7622  pwexr  7701  cnvexg  7857  resfunexgALT  7883  abrexex2g  7899  opabex3d  7900  opabex3rd  7901  frxp3  8084  suppssov1  8130  suppssov2  8131  suppssfv  8135  ralxpmap  8823  unfi  9085  imafi  9204  pwfir  9206  pwfilem  9207  residfi  9228  abrexfi  9242  ssfii  9309  wdomima2g  9478  unxpwdom2  9480  tskwe  9846  ac10ct  9928  fin23lem28  10234  fin23lem30  10236  axcclem  10351  distrlem4pr  10920  iccshftr  13389  iccshftl  13391  iccdil  13393  icccntr  13395  o1res  15467  exprmfct  16615  infpnlem1  16822  4sqlem13  16869  0ram  16932  ressval3d  17157  ismred2  17505  mreexexlem2d  17551  mreexexlem4d  17553  acsfn1c  17568  acsfn2  17569  ssclem  17726  submacs  18701  symgtset  19278  symgsubmefmndALT  19282  efgrcl  19594  cntrcmnd  19721  cntrabl  19722  dprd2da  19923  ogrpaddltrbid  20020  srgbinom  20116  irredlmul  20313  rngridlmcl  21124  lidlrsppropd  21151  rngqiprngghmlem1  21194  rngqiprnglinlem2  21199  rngqiprngimf1lem  21201  rngqiprng  21203  rngqiprngimf  21204  rngqiprngghm  21206  rngqiprngimf1  21207  rngqiprngimfo  21208  rng2idl1cntr  21212  rngqiprngfulem4  21221  rngqipring1  21223  pzriprnglem6  21393  chrcl  21431  css1  21597  issubassa  21774  ply1crng  22081  ply1ring  22130  ply1lmod  22134  oftpos  22337  tposmap  22342  0opn  22789  fctop2  22890  difopn  22919  tgrest  23044  ordtbas2  23076  ordtopn3  23081  ordtcld3  23084  t1ficld  23212  resthauslem  23248  kgentopon  23423  txbasex  23451  txcnpi  23493  txdis1cn  23520  pthaus  23523  txkgen  23537  cnmptid  23546  cnmptc  23547  cnmpt1st  23553  cnmpt2nd  23554  cnmpt2c  23555  cnmptkc  23564  txconn  23574  hmeoima  23650  hmeocld  23652  xkohmeo  23700  filufint  23805  fin1aufil  23817  flftg  23881  ptcmplem2  23938  tmdmulg  23977  tmdgsum2  23981  submtmd  23989  symgtgp  23991  ghmcnp  24000  qustgpopn  24005  qustgplem  24006  ust0  24105  nrginvrcn  24578  fsumcn  24759  fsum2cn  24760  expcn  24761  expcnOLD  24763  cnheibor  24852  evth2  24857  csscld  25147  clsocv  25148  ovoliun2  25405  volfiniun  25446  dyadmbl  25499  mbfeqalem2  25541  mbfss  25545  ismbf3d  25553  mbfadd  25560  i1f0rn  25581  mbfmul  25625  itg2seq  25641  itg2monolem2  25650  itg2monolem3  25651  itg2mono  25652  itgreval  25696  itgge0  25710  itgss3  25714  iblconst  25717  itgconst  25718  ibladdlem  25719  itgfsum  25726  iblabslem  25727  itgabs  25734  cmvth  25893  lhop1lem  25916  dvfsumle  25924  dvfsumleOLD  25925  dvfsumlem2  25931  dvfsumlem2OLD  25932  ftc1lem4  25944  itgparts  25952  itgsubstlem  25953  itgsubst  25954  plydivlem1  26199  aannenlem1  26234  taylply2  26273  taylply2OLD  26274  itgulm  26315  cxpcn  26652  cxpcnOLD  26653  resqrtcn  26657  basellem1  26989  mulogsumlem  27440  mulog2sumlem2  27444  selberg2lem  27459  pntrsumo1  27474  addsuniflem  27913  ssltmul1  28055  ssltmul2  28056  precsexlem11  28124  usgrnbcnvfv  29310  ewlksfval  29547  crctcshwlkn0  29766  pjssmii  31625  rabrexfi  32450  abrexexd  32453  mptiffisupp  32636  pfxlsw2ccat  32893  cntrcrng  33024  dfufd2lem  33487  ply1degltdimlem  33595  fldgenfldext  33641  fldextrspunlem2  33650  lmatfval  33787  pl1cn  33928  esumcvg  34059  esumcvgsum  34061  sigaval  34084  sigaclfu2  34094  sigapildsys  34135  ldgenpisys  34139  measinb2  34196  braew  34215  unelcarsg  34286  carsgclctunlem2  34293  sibfof  34314  sitgclg  34316  orrvcoel  34440  orrvccel  34441  fsum2dsub  34581  fineqvpow  35077  subfaclefac  35159  cvmsss2  35257  cvmopnlem  35261  satf0suclem  35358  mpstrcl  35524  elmpps  35556  hmeoclda  36317  bj-1uplex  36992  bj-2uplex  37006  icoreclin  37341  broucube  37644  mblfinlem1  37647  cnambfre  37658  ibladdnclem  37666  iblabsnclem  37673  itgabsnc  37679  ftc1cnnclem  37681  ftc1anclem4  37686  ftc1anclem5  37687  ftc1anclem6  37688  ftc1anclem7  37689  ftc2nc  37692  areacirc  37703  zrdivrng  37943  xrnresex  38388  dalemrot  39646  dalem10  39662  arglem1N  40179  cdlemk36  40902  resopunitintvd  42009  resclunitintvd  42010  lcmineqlem2  42013  aks6d1c7lem1  42163  aks5lem2  42170  mzpconstmpt  42723  mzpresrename  42733  diophrex  42758  0dioph  42761  anrabdioph  42763  orrabdioph  42764  rabren3dioph  42798  dvradcnv2  44330  xpexb  44437  fsumcnf  45009  uzublem  45419  fprodcncf  45891  iblconstmpt  45947  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  dirkercncflem2  46095  fourierdlem47  46144  saluni  46316  sge0iunmpt  46409  sge0xaddlem2  46425  sge0xadd  46426  hoidmvlelem3  46588  ctvonmbl  46680  vonct  46684  smfaddlem2  46755  smfmullem4  46785  singoutnword  46873  aoprssdm  47196  rescofuf  49088  idfu1stalem  49095  idfu1sta  49096  idfu1a  49097  idfu2nda  49098  oppfuprcl  49199  lmddu  49662  cmddu  49663