Theorem eqeltrrid 2918

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  3eltr3g  2929  dmrnssfld  5841  oprssdm  7329  offval  7416  pwexr  7487  cnvexg  7629  resfunexgALT  7649  abrexexg  7662  abrexex2g  7665  opabex3d  7666  opabex3rd  7667  suppssov1  7862  suppssfv  7866  ralxpmap  8460  residfi  8805  imafi  8817  abrexfi  8824  ssfii  8883  wdomima2g  9050  unxpwdom2  9052  tskwe  9379  ac10ct  9460  fin23lem28  9762  fin23lem30  9764  axcclem  9879  distrlem4pr  10448  iccshftr  12873  iccshftl  12875  iccdil  12877  icccntr  12879  o1res  14917  exprmfct  16048  infpnlem1  16246  4sqlem13  16293  0ram  16356  ressval3d  16561  ismred2  16874  mreexexlem2d  16916  mreexexlem4d  16918  acsfn1c  16933  acsfn2  16934  ssclem  17089  submacs  17991  symgtset  18527  symgsubmefmndALT  18531  efgrcl  18841  cntrcmnd  18962  cntrabl  18963  dprd2da  19164  srgbinom  19295  irredlmul  19458  lidlrsppropd  20003  issubassa  20098  ply1crng  20366  ply1ring  20416  ply1lmod  20420  chrcl  20673  css1  20834  oftpos  21061  tposmap  21066  0opn  21512  fctop2  21613  difopn  21642  tgrest  21767  ordtbas2  21799  ordtopn3  21804  ordtcld3  21807  t1ficld  21935  resthauslem  21971  kgentopon  22146  txbasex  22174  txcnpi  22216  txdis1cn  22243  pthaus  22246  txkgen  22260  cnmptid  22269  cnmptc  22270  cnmpt1st  22276  cnmpt2nd  22277  cnmpt2c  22278  cnmptkc  22287  txconn  22297  hmeoima  22373  hmeocld  22375  xkohmeo  22423  filufint  22528  fin1aufil  22540  flftg  22604  ptcmplem2  22661  tmdmulg  22700  tmdgsum2  22704  submtmd  22712  symgtgp  22714  ghmcnp  22723  qustgpopn  22728  qustgplem  22729  ust0  22828  nrginvrcn  23301  fsumcn  23478  fsum2cn  23479  expcn  23480  cnheibor  23559  evth2  23564  csscld  23852  clsocv  23853  ovoliun2  24107  volfiniun  24148  dyadmbl  24201  mbfeqalem2  24243  mbfss  24247  ismbf3d  24255  mbfadd  24262  i1f0rn  24283  mbfmul  24327  itg2seq  24343  itg2monolem2  24352  itg2monolem3  24353  itg2mono  24354  itgreval  24397  itgge0  24411  itgss3  24415  iblconst  24418  itgconst  24419  ibladdlem  24420  itgfsum  24427  iblabslem  24428  itgabs  24435  lhop1lem  24610  dvfsumle  24618  dvfsumlem2  24624  ftc1lem4  24636  itgparts  24644  itgsubstlem  24645  itgsubst  24646  plydivlem1  24882  aannenlem1  24917  taylply2  24956  itgulm  24996  cxpcn  25326  resqrtcn  25330  basellem1  25658  mulogsumlem  26107  mulog2sumlem2  26111  selberg2lem  26126  pntrsumo1  26141  usgrnbcnvfv  27147  ewlksfval  27383  crctcshwlkn0  27599  pjssmii  29458  abrexexd  30269  pfxlsw2ccat  30626  cntrcrng  30697  ogrpaddltrbid  30721  lmatfval  31079  pl1cn  31198  esumcvg  31345  esumcvgsum  31347  sigaval  31370  sigaclfu2  31380  sigapildsys  31421  ldgenpisys  31425  measinb2  31482  braew  31501  unelcarsg  31570  carsgclctunlem2  31577  sibfof  31598  sitgclg  31600  orrvcoel  31723  orrvccel  31724  fsum2dsub  31878  subfaclefac  32423  cvmsss2  32521  cvmopnlem  32525  satf0suclem  32622  mpstrcl  32788  elmpps  32820  hmeoclda  33681  bj-1uplex  34323  bj-2uplex  34337  icoreclin  34641  broucube  34941  mblfinlem1  34944  cnambfre  34955  ibladdnclem  34963  iblabsnclem  34970  itgabsnc  34976  ftc1cnnclem  34980  ftc1anclem4  34985  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem7  34988  ftc2nc  34991  areacirc  35002  zrdivrng  35246  xrnresex  35669  dalemrot  36808  dalem10  36824  arglem1N  37341  cdlemk36  38064  mzpconstmpt  39386  mzpresrename  39396  diophrex  39421  0dioph  39424  anrabdioph  39426  orrabdioph  39427  rabren3dioph  39461  iunrelexp0  40096  dvradcnv2  40728  xpexb  40835  fsumcnf  41327  uzublem  41753  fprodcncf  42233  iblconstmpt  42290  itgiccshift  42314  itgperiod  42315  itgsbtaddcnst  42316  dirkercncflem2  42438  fourierdlem47  42487  saluni  42658  sge0iunmpt  42749  sge0xaddlem2  42765  sge0xadd  42766  hoidmvlelem3  42928  ctvonmbl  43020  vonct  43024  smfaddlem2  43089  smfmullem4  43118  aoprssdm  43450