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  5925  oprssdm  7543  offval  7635  pwexr  7714  cnvexg  7870  resfunexgALT  7896  abrexex2g  7912  opabex3d  7913  opabex3rd  7914  frxp3  8096  suppssov1  8142  suppssov2  8143  suppssfv  8147  ralxpmap  8839  unfi  9100  imafi  9220  pwfir  9222  pwfilem  9223  residfi  9243  abrexfi  9257  ssfii  9327  wdomima2g  9496  unxpwdom2  9498  tskwe  9869  ac10ct  9951  fin23lem28  10257  fin23lem30  10259  axcclem  10374  distrlem4pr  10944  iccshftr  13434  iccshftl  13436  iccdil  13438  icccntr  13440  o1res  15517  exprmfct  16669  infpnlem1  16876  4sqlem13  16923  0ram  16986  ressval3d  17211  ismred2  17560  mreexexlem2d  17606  mreexexlem4d  17608  acsfn1c  17623  acsfn2  17624  ssclem  17781  submacs  18790  symgtset  19369  symgsubmefmndALT  19373  efgrcl  19685  cntrcmnd  19812  cntrabl  19813  dprd2da  20014  ogrpaddltrbid  20111  srgbinom  20207  irredlmul  20403  rngridlmcl  21211  lidlrsppropd  21238  rngqiprngghmlem1  21281  rngqiprnglinlem2  21286  rngqiprngimf1lem  21288  rngqiprng  21290  rngqiprngimf  21291  rngqiprngghm  21293  rngqiprngimf1  21294  rngqiprngimfo  21295  rng2idl1cntr  21299  rngqiprngfulem4  21308  rngqipring1  21310  pzriprnglem6  21480  chrcl  21518  css1  21684  issubassa  21861  ply1crng  22176  ply1ring  22225  ply1lmod  22229  oftpos  22431  tposmap  22436  0opn  22883  fctop2  22984  difopn  23013  tgrest  23138  ordtbas2  23170  ordtopn3  23175  ordtcld3  23178  t1ficld  23306  resthauslem  23342  kgentopon  23517  txbasex  23545  txcnpi  23587  txdis1cn  23614  pthaus  23617  txkgen  23631  cnmptid  23640  cnmptc  23641  cnmpt1st  23647  cnmpt2nd  23648  cnmpt2c  23649  cnmptkc  23658  txconn  23668  hmeoima  23744  hmeocld  23746  xkohmeo  23794  filufint  23899  fin1aufil  23911  flftg  23975  ptcmplem2  24032  tmdmulg  24071  tmdgsum2  24075  submtmd  24083  symgtgp  24085  ghmcnp  24094  qustgpopn  24099  qustgplem  24100  ust0  24199  nrginvrcn  24671  fsumcn  24851  fsum2cn  24852  expcn  24853  cnheibor  24936  evth2  24941  csscld  25230  clsocv  25231  ovoliun2  25487  volfiniun  25528  dyadmbl  25581  mbfeqalem2  25623  mbfss  25627  ismbf3d  25635  mbfadd  25642  i1f0rn  25663  mbfmul  25707  itg2seq  25723  itg2monolem2  25732  itg2monolem3  25733  itg2mono  25734  itgreval  25778  itgge0  25792  itgss3  25796  iblconst  25799  itgconst  25800  ibladdlem  25801  itgfsum  25808  iblabslem  25809  itgabs  25816  cmvth  25972  lhop1lem  25994  dvfsumle  26002  dvfsumlem2  26008  ftc1lem4  26020  itgparts  26028  itgsubstlem  26029  itgsubst  26030  plydivlem1  26274  aannenlem1  26309  taylply2  26348  taylply2OLD  26349  itgulm  26390  cxpcn  26726  resqrtcn  26730  basellem1  27062  mulogsumlem  27512  mulog2sumlem2  27516  selberg2lem  27531  pntrsumo1  27546  addsuniflem  28011  sltmuls1  28157  sltmuls2  28158  precsexlem11  28227  usgrnbcnvfv  29452  ewlksfval  29689  crctcshwlkn0  29908  pjssmii  31771  rabrexfi  32595  abrexexd  32598  mptiffisupp  32785  pfxlsw2ccat  33029  gsummulsubdishift2s  33151  cntrcrng  33161  dfufd2lem  33628  vietalem  33742  ply1degltdimlem  33786  fldgenfldext  33832  fldextrspunlem2  33841  lmatfval  33978  pl1cn  34119  esumcvg  34250  esumcvgsum  34252  sigaval  34275  sigaclfu2  34285  sigapildsys  34326  ldgenpisys  34330  measinb2  34387  braew  34406  unelcarsg  34476  carsgclctunlem2  34483  sibfof  34504  sitgclg  34506  orrvcoel  34630  orrvccel  34631  fsum2dsub  34771  fineqvpow  35279  subfaclefac  35378  cvmsss2  35476  cvmopnlem  35480  satf0suclem  35577  mpstrcl  35743  elmpps  35775  hmeoclda  36535  bj-1uplex  37335  bj-2uplex  37349  icoreclin  37691  broucube  37993  mblfinlem1  37996  cnambfre  38007  ibladdnclem  38015  iblabsnclem  38022  itgabsnc  38028  ftc1cnnclem  38030  ftc1anclem4  38035  ftc1anclem5  38036  ftc1anclem6  38037  ftc1anclem7  38038  ftc2nc  38041  areacirc  38052  zrdivrng  38292  xrnresex  38768  dalemrot  40121  dalem10  40137  arglem1N  40654  cdlemk36  41377  resopunitintvd  42483  resclunitintvd  42484  lcmineqlem2  42487  aks6d1c7lem1  42637  aks5lem2  42644  mzpconstmpt  43190  mzpresrename  43200  diophrex  43225  0dioph  43228  anrabdioph  43230  orrabdioph  43231  rabren3dioph  43265  dvradcnv2  44796  xpexb  44902  fsumcnf  45474  uzublem  45880  fprodcncf  46350  iblconstmpt  46406  itgiccshift  46430  itgperiod  46431  itgsbtaddcnst  46432  dirkercncflem2  46554  fourierdlem47  46603  saluni  46775  sge0iunmpt  46868  sge0xaddlem2  46884  sge0xadd  46885  hoicvr  46998  hoidmvlelem3  47047  ctvonmbl  47139  vonct  47143  smfaddlem2  47214  smfmullem4  47244  aoprssdm  47666  rescofuf  49584  idfu1stalem  49591  idfu1sta  49592  idfu1a  49593  idfu2nda  49594  oppfuprcl  49695  lmddu  50158  cmddu  50159