Theorem eqeltrrid 2870

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  3eltr3g  2881  dmrnssfld  5966  oprssdm  7601  offval  7693  pwexr  7770  cnvexg  7927  resfunexgALT  7951  abrexex2g  7967  opabex3d  7968  opabex3rd  7969  frxp3  8153  suppssov1  8199  suppssov2  8200  suppssfv  8204  ralxpmap  8900  unfi  9162  imafi  9282  pwfir  9283  pwfilem  9284  resfnfinfin  9301  residfi  9302  abrexfi  9316  ssfii  9386  wdomima2g  9555  unxpwdom2  9557  tskwe  9952  fin23lem28  10339  fin23lem30  10341  axcclem  10456  distrlem4pr  11028  iccshftr  13531  iccshftl  13533  iccdil  13535  icccntr  13537  o1res  15637  exprmfct  16787  infpnlem1  16994  4sqlem13  17041  0ram  17104  ressval3d  17330  ismred2  17679  mreexexlem2d  17725  mreexexlem4d  17727  acsfn1c  17742  acsfn2  17743  ssclem  17900  submacs  18925  symgtset  19515  symgsubmefmndALT  19519  efgrcl  19831  cntrcmnd  19958  cntrabl  19959  dprd2da  20160  ogrpaddltrbid  20257  srgbinom  20359  irredlmul  20558  rngridlmcl  21394  lidlrsppropd  21430  rngqiprngghmlem1  21479  rngqiprnglinlem2  21484  rngqiprngimf1lem  21486  rngqiprng  21488  rngqiprngimf  21489  rngqiprngghm  21491  rngqiprngimf1  21492  rngqiprngimfo  21493  rng2idl1cntr  21497  rngqiprngfulem4  21506  rngqipring1  21508  pzriprnglem6  21688  chrcl  21726  css1  21892  issubassa  22069  ply1crng  22410  ply1ring  22459  ply1lmod  22463  oftpos  22661  tposmap  22666  0opn  23113  fctop2  23214  difopn  23243  tgrest  23368  ordtbas2  23400  ordtopn3  23405  ordtcld3  23408  t1ficld  23536  resthauslem  23572  kgentopon  23748  txbasex  23776  txcnpi  23818  txdis1cn  23845  pthaus  23848  txkgen  23862  cnmptid  23871  cnmptc  23872  cnmpt1st  23878  cnmpt2nd  23879  cnmpt2c  23880  cnmptkc  23889  txconn  23899  hmeoima  23975  hmeocld  23977  xkohmeo  24025  filufint  24130  fin1aufil  24142  flftg  24206  ptcmplem2  24263  tmdmulg  24302  tmdgsum2  24306  submtmd  24314  symgtgp  24316  ghmcnp  24325  qustgpopn  24330  qustgplem  24331  ust0  24430  nrginvrcn  24902  fsumcn  25082  fsum2cn  25083  expcn  25084  cnheibor  25167  evth2  25172  csscld  25461  clsocv  25462  ovoliun2  25718  volfiniun  25759  dyadmbl  25812  mbfeqalem2  25854  mbfss  25858  ismbf3d  25866  mbfadd  25873  i1f0rn  25894  mbfmul  25938  itg2seq  25954  itg2monolem2  25963  itg2monolem3  25964  itg2mono  25965  itgreval  26009  itgge0  26023  itgss3  26027  iblconst  26030  itgconst  26031  ibladdlem  26032  itgfsum  26039  iblabslem  26040  itgabs  26047  cmvth  26203  lhop1lem  26225  dvfsumle  26233  dvfsumlem2  26239  ftc1lem4  26251  itgparts  26259  itgsubstlem  26260  itgsubst  26261  plydivlem1  26507  aannenlem1  26544  taylply2  26584  itgulm  26624  cxpcn  26963  resqrtcn  26967  basellem1  27298  mulogsumlem  27748  mulog2sumlem2  27752  selberg2lem  27767  pntrsumo1  27782  addsuniflem  28247  sltmuls1  28393  sltmuls2  28394  precsexlem11  28463  usgrnbcnvfv  29775  ewlksfval  30011  crctcshwlkn0  30239  pjssmii  32106  rabrexfi  32925  abrexexd  32928  mptiffisupp  33111  pfxlsw2ccat  33338  gsummulsubdishift2s  33457  cntrcrng  33467  dfufd2lem  33905  selvply1rhmlemb  33975  vietalem  34035  ply1degltdimlem  34078  fldgenfldext  34124  fldextrspunlem2  34133  lmatfval  34270  pl1cn  34411  esumcvg  34542  esumcvgsum  34544  sigaval  34567  sigaclfu2  34577  sigapildsys  34619  ldgenpisys  34623  measinb2  34680  braew  34699  unelcarsg  34769  carsgclctunlem2  34776  sibfof  34797  sitgclg  34799  orrvcoel  34923  orrvccel  34924  fsum2dsub  35061  fineqvpow  35587  subfaclefac  35707  cvmsss2  35805  cvmopnlem  35809  satf0suclem  35906  mpstrcl  36072  elmpps  36104  hmeoclda  36903  bj-1uplex  37703  bj-2uplex  37717  icoreclin  38062  broucube  38364  mblfinlem1  38367  cnambfre  38378  ibladdnclem  38386  iblabsnclem  38393  itgabsnc  38399  ftc1cnnclem  38401  ftc1anclem4  38406  ftc1anclem5  38407  ftc1anclem6  38408  ftc1anclem7  38409  ftc2nc  38412  areacirc  38423  zrdivrng  38664  xrnresex  39138  dalemrot  40491  dalem10  40507  arglem1N  41024  cdlemk36  41747  resopunitintvd  42853  resclunitintvd  42854  lcmineqlem2  42857  aks6d1c7lem1  43007  aks5lem2  43014  mzpconstmpt  43531  mzpresrename  43541  diophrex  43566  0dioph  43569  anrabdioph  43571  orrabdioph  43572  rabren3dioph  43602  dvradcnv2  45117  xpexb  45222  fsumcnf  45801  uzublem  46204  fprodcncf  46674  iblconstmpt  46730  itgiccshift  46754  itgperiod  46755  itgsbtaddcnst  46756  dirkercncflem2  46878  fourierdlem47  46927  saluni  47099  sge0iunmpt  47192  sge0xaddlem2  47208  sge0xadd  47209  hoicvr  47322  hoidmvlelem3  47371  ctvonmbl  47463  vonct  47467  smfaddlem2  47538  smfmullem4  47568  aoprssdm  47999  rescofuf  49930  idfu1stalem  49937  idfu1sta  49938  idfu1a  49939  idfu2nda  49940  oppfuprcl  50041  lmddu  50504  cmddu  50505