Theorem eqeltrrid 2843

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  3eltr3g  2854  dmrnssfld  5986  oprssdm  7613  offval  7705  pwexr  7783  cnvexg  7946  resfunexgALT  7970  abrexexgOLD  7984  abrexex2g  7987  opabex3d  7988  opabex3rd  7989  frxp3  8174  suppssov1  8220  suppssov2  8221  suppssfv  8225  ralxpmap  8934  unfi  9209  imafi  9350  pwfir  9352  pwfilem  9353  residfi  9375  abrexfi  9389  ssfii  9456  wdomima2g  9623  unxpwdom2  9625  tskwe  9987  ac10ct  10071  fin23lem28  10377  fin23lem30  10379  axcclem  10494  distrlem4pr  11063  iccshftr  13522  iccshftl  13524  iccdil  13526  icccntr  13528  o1res  15592  exprmfct  16737  infpnlem1  16943  4sqlem13  16990  0ram  17053  ressval3d  17291  ressval3dOLD  17292  ismred2  17647  mreexexlem2d  17689  mreexexlem4d  17691  acsfn1c  17706  acsfn2  17707  ssclem  17866  submacs  18852  symgtset  19431  symgsubmefmndALT  19435  efgrcl  19747  cntrcmnd  19874  cntrabl  19875  dprd2da  20076  srgbinom  20248  irredlmul  20444  rngridlmcl  21244  lidlrsppropd  21271  rngqiprngghmlem1  21314  rngqiprnglinlem2  21319  rngqiprngimf1lem  21321  rngqiprng  21323  rngqiprngimf  21324  rngqiprngghm  21326  rngqiprngimf1  21327  rngqiprngimfo  21328  rng2idl1cntr  21332  rngqiprngfulem4  21341  rngqipring1  21343  pzriprnglem6  21514  chrcl  21556  css1  21725  issubassa  21904  ply1crng  22215  ply1ring  22264  ply1lmod  22268  oftpos  22473  tposmap  22478  0opn  22925  fctop2  23027  difopn  23057  tgrest  23182  ordtbas2  23214  ordtopn3  23219  ordtcld3  23222  t1ficld  23350  resthauslem  23386  kgentopon  23561  txbasex  23589  txcnpi  23631  txdis1cn  23658  pthaus  23661  txkgen  23675  cnmptid  23684  cnmptc  23685  cnmpt1st  23691  cnmpt2nd  23692  cnmpt2c  23693  cnmptkc  23702  txconn  23712  hmeoima  23788  hmeocld  23790  xkohmeo  23838  filufint  23943  fin1aufil  23955  flftg  24019  ptcmplem2  24076  tmdmulg  24115  tmdgsum2  24119  submtmd  24127  symgtgp  24129  ghmcnp  24138  qustgpopn  24143  qustgplem  24144  ust0  24243  nrginvrcn  24728  fsumcn  24907  fsum2cn  24908  expcn  24909  expcnOLD  24911  cnheibor  25000  evth2  25005  csscld  25296  clsocv  25297  ovoliun2  25554  volfiniun  25595  dyadmbl  25648  mbfeqalem2  25690  mbfss  25694  ismbf3d  25702  mbfadd  25709  i1f0rn  25730  mbfmul  25775  itg2seq  25791  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  itgreval  25846  itgge0  25860  itgss3  25864  iblconst  25867  itgconst  25868  ibladdlem  25869  itgfsum  25876  iblabslem  25877  itgabs  25884  cmvth  26043  lhop1lem  26066  dvfsumle  26074  dvfsumleOLD  26075  dvfsumlem2  26081  dvfsumlem2OLD  26082  ftc1lem4  26094  itgparts  26102  itgsubstlem  26103  itgsubst  26104  plydivlem1  26349  aannenlem1  26384  taylply2  26423  taylply2OLD  26424  itgulm  26465  cxpcn  26801  cxpcnOLD  26802  resqrtcn  26806  basellem1  27138  mulogsumlem  27589  mulog2sumlem2  27593  selberg2lem  27608  pntrsumo1  27623  addsuniflem  28048  ssltmul1  28187  ssltmul2  28188  precsexlem11  28255  usgrnbcnvfv  29396  ewlksfval  29633  crctcshwlkn0  29850  pjssmii  31709  rabrexfi  32533  abrexexd  32536  mptiffisupp  32707  pfxlsw2ccat  32919  cntrcrng  33055  ogrpaddltrbid  33079  dfufd2lem  33556  ply1degltdimlem  33649  fldgenfldext  33692  lmatfval  33774  pl1cn  33915  esumcvg  34066  esumcvgsum  34068  sigaval  34091  sigaclfu2  34101  sigapildsys  34142  ldgenpisys  34146  measinb2  34203  braew  34222  unelcarsg  34293  carsgclctunlem2  34300  sibfof  34321  sitgclg  34323  orrvcoel  34446  orrvccel  34447  fsum2dsub  34600  fineqvpow  35088  subfaclefac  35160  cvmsss2  35258  cvmopnlem  35262  satf0suclem  35359  mpstrcl  35525  elmpps  35557  hmeoclda  36315  bj-1uplex  36990  bj-2uplex  37004  icoreclin  37339  broucube  37640  mblfinlem1  37643  cnambfre  37654  ibladdnclem  37662  iblabsnclem  37669  itgabsnc  37675  ftc1cnnclem  37677  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc2nc  37688  areacirc  37699  zrdivrng  37939  xrnresex  38387  dalemrot  39639  dalem10  39655  arglem1N  40172  cdlemk36  40895  resopunitintvd  42007  resclunitintvd  42008  lcmineqlem2  42011  aks6d1c7lem1  42161  aks5lem2  42168  mzpconstmpt  42727  mzpresrename  42737  diophrex  42762  0dioph  42765  anrabdioph  42767  orrabdioph  42768  rabren3dioph  42802  dvradcnv2  44342  xpexb  44449  fsumcnf  44958  uzublem  45379  fprodcncf  45855  iblconstmpt  45911  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  dirkercncflem2  46059  fourierdlem47  46108  saluni  46280  sge0iunmpt  46373  sge0xaddlem2  46389  sge0xadd  46390  hoidmvlelem3  46552  ctvonmbl  46644  vonct  46648  smfaddlem2  46719  smfmullem4  46749  singoutnword  46835  aoprssdm  47151