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  5937  oprssdm  7570  offval  7662  pwexr  7741  cnvexg  7900  resfunexgALT  7926  abrexexgOLD  7940  abrexex2g  7943  opabex3d  7944  opabex3rd  7945  frxp3  8130  suppssov1  8176  suppssov2  8177  suppssfv  8181  ralxpmap  8869  unfi  9135  imafi  9264  pwfir  9266  pwfilem  9267  residfi  9289  abrexfi  9303  ssfii  9370  wdomima2g  9539  unxpwdom2  9541  tskwe  9903  ac10ct  9987  fin23lem28  10293  fin23lem30  10295  axcclem  10410  distrlem4pr  10979  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  o1res  15526  exprmfct  16674  infpnlem1  16881  4sqlem13  16928  0ram  16991  ressval3d  17216  ismred2  17564  mreexexlem2d  17606  mreexexlem4d  17608  acsfn1c  17623  acsfn2  17624  ssclem  17781  submacs  18754  symgtset  19329  symgsubmefmndALT  19333  efgrcl  19645  cntrcmnd  19772  cntrabl  19773  dprd2da  19974  srgbinom  20140  irredlmul  20337  rngridlmcl  21127  lidlrsppropd  21154  rngqiprngghmlem1  21197  rngqiprnglinlem2  21202  rngqiprngimf1lem  21204  rngqiprng  21206  rngqiprngimf  21207  rngqiprngghm  21209  rngqiprngimf1  21210  rngqiprngimfo  21211  rng2idl1cntr  21215  rngqiprngfulem4  21224  rngqipring1  21226  pzriprnglem6  21396  chrcl  21434  css1  21599  issubassa  21776  ply1crng  22083  ply1ring  22132  ply1lmod  22136  oftpos  22339  tposmap  22344  0opn  22791  fctop2  22892  difopn  22921  tgrest  23046  ordtbas2  23078  ordtopn3  23083  ordtcld3  23086  t1ficld  23214  resthauslem  23250  kgentopon  23425  txbasex  23453  txcnpi  23495  txdis1cn  23522  pthaus  23525  txkgen  23539  cnmptid  23548  cnmptc  23549  cnmpt1st  23555  cnmpt2nd  23556  cnmpt2c  23557  cnmptkc  23566  txconn  23576  hmeoima  23652  hmeocld  23654  xkohmeo  23702  filufint  23807  fin1aufil  23819  flftg  23883  ptcmplem2  23940  tmdmulg  23979  tmdgsum2  23983  submtmd  23991  symgtgp  23993  ghmcnp  24002  qustgpopn  24007  qustgplem  24008  ust0  24107  nrginvrcn  24580  fsumcn  24761  fsum2cn  24762  expcn  24763  expcnOLD  24765  cnheibor  24854  evth2  24859  csscld  25149  clsocv  25150  ovoliun2  25407  volfiniun  25448  dyadmbl  25501  mbfeqalem2  25543  mbfss  25547  ismbf3d  25555  mbfadd  25562  i1f0rn  25583  mbfmul  25627  itg2seq  25643  itg2monolem2  25652  itg2monolem3  25653  itg2mono  25654  itgreval  25698  itgge0  25712  itgss3  25716  iblconst  25719  itgconst  25720  ibladdlem  25721  itgfsum  25728  iblabslem  25729  itgabs  25736  cmvth  25895  lhop1lem  25918  dvfsumle  25926  dvfsumleOLD  25927  dvfsumlem2  25933  dvfsumlem2OLD  25934  ftc1lem4  25946  itgparts  25954  itgsubstlem  25955  itgsubst  25956  plydivlem1  26201  aannenlem1  26236  taylply2  26275  taylply2OLD  26276  itgulm  26317  cxpcn  26654  cxpcnOLD  26655  resqrtcn  26659  basellem1  26991  mulogsumlem  27442  mulog2sumlem2  27446  selberg2lem  27461  pntrsumo1  27476  addsuniflem  27908  ssltmul1  28050  ssltmul2  28051  precsexlem11  28119  usgrnbcnvfv  29292  ewlksfval  29529  crctcshwlkn0  29751  pjssmii  31610  rabrexfi  32435  abrexexd  32438  mptiffisupp  32616  pfxlsw2ccat  32872  cntrcrng  33010  ogrpaddltrbid  33034  dfufd2lem  33520  ply1degltdimlem  33618  fldgenfldext  33663  fldextrspunlem2  33672  lmatfval  33804  pl1cn  33945  esumcvg  34076  esumcvgsum  34078  sigaval  34101  sigaclfu2  34111  sigapildsys  34152  ldgenpisys  34156  measinb2  34213  braew  34232  unelcarsg  34303  carsgclctunlem2  34310  sibfof  34331  sitgclg  34333  orrvcoel  34457  orrvccel  34458  fsum2dsub  34598  fineqvpow  35086  subfaclefac  35163  cvmsss2  35261  cvmopnlem  35265  satf0suclem  35362  mpstrcl  35528  elmpps  35560  hmeoclda  36321  bj-1uplex  36996  bj-2uplex  37010  icoreclin  37345  broucube  37648  mblfinlem1  37651  cnambfre  37662  ibladdnclem  37670  iblabsnclem  37677  itgabsnc  37683  ftc1cnnclem  37685  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc2nc  37696  areacirc  37707  zrdivrng  37947  xrnresex  38392  dalemrot  39651  dalem10  39667  arglem1N  40184  cdlemk36  40907  resopunitintvd  42014  resclunitintvd  42015  lcmineqlem2  42018  aks6d1c7lem1  42168  aks5lem2  42175  mzpconstmpt  42728  mzpresrename  42738  diophrex  42763  0dioph  42766  anrabdioph  42768  orrabdioph  42769  rabren3dioph  42803  dvradcnv2  44336  xpexb  44443  fsumcnf  45015  uzublem  45426  fprodcncf  45898  iblconstmpt  45954  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  dirkercncflem2  46102  fourierdlem47  46151  saluni  46323  sge0iunmpt  46416  sge0xaddlem2  46432  sge0xadd  46433  hoidmvlelem3  46595  ctvonmbl  46687  vonct  46691  smfaddlem2  46762  smfmullem4  46792  singoutnword  46880  aoprssdm  47203  rescofuf  49082  idfu1stalem  49089  idfu1sta  49090  idfu1a  49091  idfu2nda  49092  oppfuprcl  49193  lmddu  49656  cmddu  49657