Theorem eqeltrrid 2838

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  3eltr3g  2849  dmrnssfld  5969  oprssdm  7587  offval  7678  pwexr  7751  cnvexg  7914  resfunexgALT  7933  abrexexgOLD  7947  abrexex2g  7950  opabex3d  7951  opabex3rd  7952  frxp3  8136  suppssov1  8182  suppssfv  8186  ralxpmap  8889  unfi  9171  pwfir  9175  pwfilem  9176  residfi  9332  imafiALT  9344  abrexfi  9351  ssfii  9413  wdomima2g  9580  unxpwdom2  9582  tskwe  9944  ac10ct  10028  fin23lem28  10334  fin23lem30  10336  axcclem  10451  distrlem4pr  11020  iccshftr  13462  iccshftl  13464  iccdil  13466  icccntr  13468  o1res  15503  exprmfct  16640  infpnlem1  16842  4sqlem13  16889  0ram  16952  ressval3d  17190  ressval3dOLD  17191  ismred2  17546  mreexexlem2d  17588  mreexexlem4d  17590  acsfn1c  17605  acsfn2  17606  ssclem  17765  submacs  18707  symgtset  19266  symgsubmefmndALT  19270  efgrcl  19582  cntrcmnd  19709  cntrabl  19710  dprd2da  19911  srgbinom  20053  irredlmul  20241  lidlrsppropd  20854  chrcl  21077  css1  21242  issubassa  21420  ply1crng  21721  ply1ring  21769  ply1lmod  21773  oftpos  21953  tposmap  21958  0opn  22405  fctop2  22507  difopn  22537  tgrest  22662  ordtbas2  22694  ordtopn3  22699  ordtcld3  22702  t1ficld  22830  resthauslem  22866  kgentopon  23041  txbasex  23069  txcnpi  23111  txdis1cn  23138  pthaus  23141  txkgen  23155  cnmptid  23164  cnmptc  23165  cnmpt1st  23171  cnmpt2nd  23172  cnmpt2c  23173  cnmptkc  23182  txconn  23192  hmeoima  23268  hmeocld  23270  xkohmeo  23318  filufint  23423  fin1aufil  23435  flftg  23499  ptcmplem2  23556  tmdmulg  23595  tmdgsum2  23599  submtmd  23607  symgtgp  23609  ghmcnp  23618  qustgpopn  23623  qustgplem  23624  ust0  23723  nrginvrcn  24208  fsumcn  24385  fsum2cn  24386  expcn  24387  cnheibor  24470  evth2  24475  csscld  24765  clsocv  24766  ovoliun2  25022  volfiniun  25063  dyadmbl  25116  mbfeqalem2  25158  mbfss  25162  ismbf3d  25170  mbfadd  25177  i1f0rn  25198  mbfmul  25243  itg2seq  25259  itg2monolem2  25268  itg2monolem3  25269  itg2mono  25270  itgreval  25313  itgge0  25327  itgss3  25331  iblconst  25334  itgconst  25335  ibladdlem  25336  itgfsum  25343  iblabslem  25344  itgabs  25351  lhop1lem  25529  dvfsumle  25537  dvfsumlem2  25543  ftc1lem4  25555  itgparts  25563  itgsubstlem  25564  itgsubst  25565  plydivlem1  25805  aannenlem1  25840  taylply2  25879  itgulm  25919  cxpcn  26250  resqrtcn  26254  basellem1  26582  mulogsumlem  27031  mulog2sumlem2  27035  selberg2lem  27050  pntrsumo1  27065  addsuniflem  27481  ssltmul1  27599  ssltmul2  27600  precsexlem11  27660  usgrnbcnvfv  28619  ewlksfval  28855  crctcshwlkn0  29072  pjssmii  30929  abrexexd  31741  mptiffisupp  31910  pfxlsw2ccat  32111  cntrcrng  32209  ogrpaddltrbid  32233  ply1degltdimlem  32702  lmatfval  32789  pl1cn  32930  esumcvg  33079  esumcvgsum  33081  sigaval  33104  sigaclfu2  33114  sigapildsys  33155  ldgenpisys  33159  measinb2  33216  braew  33235  unelcarsg  33306  carsgclctunlem2  33313  sibfof  33334  sitgclg  33336  orrvcoel  33459  orrvccel  33460  fsum2dsub  33614  fineqvpow  34091  subfaclefac  34162  cvmsss2  34260  cvmopnlem  34264  satf0suclem  34361  mpstrcl  34527  elmpps  34559  gg-expcn  35159  gg-cmvth  35176  gg-dvfsumle  35177  gg-dvfsumlem2  35178  gg-cxpcn  35179  hmeoclda  35213  bj-1uplex  35884  bj-2uplex  35898  icoreclin  36233  broucube  36517  mblfinlem1  36520  cnambfre  36531  ibladdnclem  36539  iblabsnclem  36546  itgabsnc  36552  ftc1cnnclem  36554  ftc1anclem4  36559  ftc1anclem5  36560  ftc1anclem6  36561  ftc1anclem7  36562  ftc2nc  36565  areacirc  36576  zrdivrng  36816  xrnresex  37271  dalemrot  38523  dalem10  38539  arglem1N  39056  cdlemk36  39779  resopunitintvd  40886  resclunitintvd  40887  lcmineqlem2  40890  mzpconstmpt  41468  mzpresrename  41478  diophrex  41503  0dioph  41506  anrabdioph  41508  orrabdioph  41509  rabren3dioph  41543  dvradcnv2  43096  xpexb  43203  fsumcnf  43695  uzublem  44130  fprodcncf  44606  iblconstmpt  44662  itgiccshift  44686  itgperiod  44687  itgsbtaddcnst  44688  dirkercncflem2  44810  fourierdlem47  44859  saluni  45031  sge0iunmpt  45124  sge0xaddlem2  45140  sge0xadd  45141  hoidmvlelem3  45303  ctvonmbl  45395  vonct  45399  smfaddlem2  45470  smfmullem4  45500  singoutnword  45586  aoprssdm  45900  rngridlmcl  46739  rngqiprngghmlem1  46762  rngqiprnglinlem2  46767  rngqiprngimf1lem  46769  rngqiprng  46771  rngqiprngimf  46772  rngqiprngghm  46774  rngqiprngimf1  46775  rngqiprngimfo  46776  rng2idl1cntr  46780  rngqiprngfulem4  46789  rngqipring1  46791  pzriprnglem6  46800