Theorem eqeltrrid 2849

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  3eltr3g  2860  dmrnssfld  5996  oprssdm  7631  offval  7723  pwexr  7800  cnvexg  7964  resfunexgALT  7988  abrexexgOLD  8002  abrexex2g  8005  opabex3d  8006  opabex3rd  8007  frxp3  8192  suppssov1  8238  suppssov2  8239  suppssfv  8243  ralxpmap  8954  unfi  9238  imafi  9381  pwfir  9383  pwfilem  9384  residfi  9406  abrexfi  9422  ssfii  9488  wdomima2g  9655  unxpwdom2  9657  tskwe  10019  ac10ct  10103  fin23lem28  10409  fin23lem30  10411  axcclem  10526  distrlem4pr  11095  iccshftr  13546  iccshftl  13548  iccdil  13550  icccntr  13552  o1res  15606  exprmfct  16751  infpnlem1  16957  4sqlem13  17004  0ram  17067  ressval3d  17305  ressval3dOLD  17306  ismred2  17661  mreexexlem2d  17703  mreexexlem4d  17705  acsfn1c  17720  acsfn2  17721  ssclem  17880  submacs  18862  symgtset  19441  symgsubmefmndALT  19445  efgrcl  19757  cntrcmnd  19884  cntrabl  19885  dprd2da  20086  srgbinom  20258  irredlmul  20454  rngridlmcl  21250  lidlrsppropd  21277  rngqiprngghmlem1  21320  rngqiprnglinlem2  21325  rngqiprngimf1lem  21327  rngqiprng  21329  rngqiprngimf  21330  rngqiprngghm  21332  rngqiprngimf1  21333  rngqiprngimfo  21334  rng2idl1cntr  21338  rngqiprngfulem4  21347  rngqipring1  21349  pzriprnglem6  21520  chrcl  21562  css1  21731  issubassa  21910  ply1crng  22221  ply1ring  22270  ply1lmod  22274  oftpos  22479  tposmap  22484  0opn  22931  fctop2  23033  difopn  23063  tgrest  23188  ordtbas2  23220  ordtopn3  23225  ordtcld3  23228  t1ficld  23356  resthauslem  23392  kgentopon  23567  txbasex  23595  txcnpi  23637  txdis1cn  23664  pthaus  23667  txkgen  23681  cnmptid  23690  cnmptc  23691  cnmpt1st  23697  cnmpt2nd  23698  cnmpt2c  23699  cnmptkc  23708  txconn  23718  hmeoima  23794  hmeocld  23796  xkohmeo  23844  filufint  23949  fin1aufil  23961  flftg  24025  ptcmplem2  24082  tmdmulg  24121  tmdgsum2  24125  submtmd  24133  symgtgp  24135  ghmcnp  24144  qustgpopn  24149  qustgplem  24150  ust0  24249  nrginvrcn  24734  fsumcn  24913  fsum2cn  24914  expcn  24915  expcnOLD  24917  cnheibor  25006  evth2  25011  csscld  25302  clsocv  25303  ovoliun2  25560  volfiniun  25601  dyadmbl  25654  mbfeqalem2  25696  mbfss  25700  ismbf3d  25708  mbfadd  25715  i1f0rn  25736  mbfmul  25781  itg2seq  25797  itg2monolem2  25806  itg2monolem3  25807  itg2mono  25808  itgreval  25852  itgge0  25866  itgss3  25870  iblconst  25873  itgconst  25874  ibladdlem  25875  itgfsum  25882  iblabslem  25883  itgabs  25890  cmvth  26049  lhop1lem  26072  dvfsumle  26080  dvfsumleOLD  26081  dvfsumlem2  26087  dvfsumlem2OLD  26088  ftc1lem4  26100  itgparts  26108  itgsubstlem  26109  itgsubst  26110  plydivlem1  26353  aannenlem1  26388  taylply2  26427  taylply2OLD  26428  itgulm  26469  cxpcn  26805  cxpcnOLD  26806  resqrtcn  26810  basellem1  27142  mulogsumlem  27593  mulog2sumlem2  27597  selberg2lem  27612  pntrsumo1  27627  addsuniflem  28052  ssltmul1  28191  ssltmul2  28192  precsexlem11  28259  usgrnbcnvfv  29400  ewlksfval  29637  crctcshwlkn0  29854  pjssmii  31713  rabrexfi  32534  abrexexd  32537  mptiffisupp  32705  pfxlsw2ccat  32917  cntrcrng  33046  ogrpaddltrbid  33070  dfufd2lem  33542  ply1degltdimlem  33635  fldgenfldext  33678  lmatfval  33760  pl1cn  33901  esumcvg  34050  esumcvgsum  34052  sigaval  34075  sigaclfu2  34085  sigapildsys  34126  ldgenpisys  34130  measinb2  34187  braew  34206  unelcarsg  34277  carsgclctunlem2  34284  sibfof  34305  sitgclg  34307  orrvcoel  34430  orrvccel  34431  fsum2dsub  34584  fineqvpow  35072  subfaclefac  35144  cvmsss2  35242  cvmopnlem  35246  satf0suclem  35343  mpstrcl  35509  elmpps  35541  hmeoclda  36299  bj-1uplex  36974  bj-2uplex  36988  icoreclin  37323  broucube  37614  mblfinlem1  37617  cnambfre  37628  ibladdnclem  37636  iblabsnclem  37643  itgabsnc  37649  ftc1cnnclem  37651  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc2nc  37662  areacirc  37673  zrdivrng  37913  xrnresex  38362  dalemrot  39614  dalem10  39630  arglem1N  40147  cdlemk36  40870  resopunitintvd  41983  resclunitintvd  41984  lcmineqlem2  41987  aks6d1c7lem1  42137  aks5lem2  42144  mzpconstmpt  42696  mzpresrename  42706  diophrex  42731  0dioph  42734  anrabdioph  42736  orrabdioph  42737  rabren3dioph  42771  dvradcnv2  44316  xpexb  44423  fsumcnf  44921  uzublem  45345  fprodcncf  45821  iblconstmpt  45877  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  dirkercncflem2  46025  fourierdlem47  46074  saluni  46246  sge0iunmpt  46339  sge0xaddlem2  46355  sge0xadd  46356  hoidmvlelem3  46518  ctvonmbl  46610  vonct  46614  smfaddlem2  46685  smfmullem4  46715  singoutnword  46801  aoprssdm  47117