Theorem eqeltrrid 2868

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  3eltr3g  2879  dmrnssfld  5964  oprssdm  7591  offval  7683  pwexr  7760  cnvexg  7917  resfunexgALT  7941  abrexex2g  7957  opabex3d  7958  opabex3rd  7959  frxp3  8143  suppssov1  8189  suppssov2  8190  suppssfv  8194  ralxpmap  8890  unfi  9151  imafi  9271  pwfir  9272  pwfilem  9273  resfnfinfin  9290  residfi  9291  abrexfi  9305  ssfii  9375  wdomima2g  9544  unxpwdom2  9546  tskwe  9932  ac10ct  10014  fin23lem28  10319  fin23lem30  10321  axcclem  10436  distrlem4pr  11006  iccshftr  13508  iccshftl  13510  iccdil  13512  icccntr  13514  o1res  15607  exprmfct  16758  infpnlem1  16965  4sqlem13  17012  0ram  17075  ressval3d  17301  ismred2  17650  mreexexlem2d  17696  mreexexlem4d  17698  acsfn1c  17713  acsfn2  17714  ssclem  17871  submacs  18881  symgtset  19464  symgsubmefmndALT  19468  efgrcl  19780  cntrcmnd  19907  cntrabl  19908  dprd2da  20109  ogrpaddltrbid  20206  srgbinom  20308  irredlmul  20506  rngridlmcl  21342  lidlrsppropd  21378  rngqiprngghmlem1  21427  rngqiprnglinlem2  21432  rngqiprngimf1lem  21434  rngqiprng  21436  rngqiprngimf  21437  rngqiprngghm  21439  rngqiprngimf1  21440  rngqiprngimfo  21441  rng2idl1cntr  21445  rngqiprngfulem4  21454  rngqipring1  21456  pzriprnglem6  21636  chrcl  21674  css1  21840  issubassa  22017  ply1crng  22358  ply1ring  22407  ply1lmod  22411  oftpos  22609  tposmap  22614  0opn  23061  fctop2  23162  difopn  23191  tgrest  23316  ordtbas2  23348  ordtopn3  23353  ordtcld3  23356  t1ficld  23484  resthauslem  23520  kgentopon  23695  txbasex  23723  txcnpi  23765  txdis1cn  23792  pthaus  23795  txkgen  23809  cnmptid  23818  cnmptc  23819  cnmpt1st  23825  cnmpt2nd  23826  cnmpt2c  23827  cnmptkc  23836  txconn  23846  hmeoima  23922  hmeocld  23924  xkohmeo  23972  filufint  24077  fin1aufil  24089  flftg  24153  ptcmplem2  24210  tmdmulg  24249  tmdgsum2  24253  submtmd  24261  symgtgp  24263  ghmcnp  24272  qustgpopn  24277  qustgplem  24278  ust0  24377  nrginvrcn  24849  fsumcn  25029  fsum2cn  25030  expcn  25031  cnheibor  25114  evth2  25119  csscld  25408  clsocv  25409  ovoliun2  25665  volfiniun  25706  dyadmbl  25759  mbfeqalem2  25801  mbfss  25805  ismbf3d  25813  mbfadd  25820  i1f0rn  25841  mbfmul  25885  itg2seq  25901  itg2monolem2  25910  itg2monolem3  25911  itg2mono  25912  itgreval  25956  itgge0  25970  itgss3  25974  iblconst  25977  itgconst  25978  ibladdlem  25979  itgfsum  25986  iblabslem  25987  itgabs  25994  cmvth  26150  lhop1lem  26172  dvfsumle  26180  dvfsumlem2  26186  ftc1lem4  26198  itgparts  26206  itgsubstlem  26207  itgsubst  26208  plydivlem1  26454  aannenlem1  26491  taylply2  26531  itgulm  26571  cxpcn  26910  resqrtcn  26914  basellem1  27245  mulogsumlem  27695  mulog2sumlem2  27699  selberg2lem  27714  pntrsumo1  27729  addsuniflem  28194  sltmuls1  28340  sltmuls2  28341  precsexlem11  28410  usgrnbcnvfv  29715  ewlksfval  29951  crctcshwlkn0  30170  pjssmii  32033  rabrexfi  32852  abrexexd  32855  mptiffisupp  33038  pfxlsw2ccat  33270  gsummulsubdishift2s  33391  cntrcrng  33401  dfufd2lem  33839  selvply1rhmlemb  33909  vietalem  33969  ply1degltdimlem  34012  fldgenfldext  34058  fldextrspunlem2  34067  lmatfval  34204  pl1cn  34345  esumcvg  34476  esumcvgsum  34478  sigaval  34501  sigaclfu2  34511  sigapildsys  34552  ldgenpisys  34556  measinb2  34613  braew  34632  unelcarsg  34702  carsgclctunlem2  34709  sibfof  34730  sitgclg  34732  orrvcoel  34856  orrvccel  34857  fsum2dsub  34994  fineqvpow  35528  subfaclefac  35668  cvmsss2  35766  cvmopnlem  35770  satf0suclem  35867  mpstrcl  36033  elmpps  36065  hmeoclda  36864  bj-1uplex  37664  bj-2uplex  37678  icoreclin  38023  broucube  38325  mblfinlem1  38328  cnambfre  38339  ibladdnclem  38347  iblabsnclem  38354  itgabsnc  38360  ftc1cnnclem  38362  ftc1anclem4  38367  ftc1anclem5  38368  ftc1anclem6  38369  ftc1anclem7  38370  ftc2nc  38373  areacirc  38384  zrdivrng  38624  xrnresex  39098  dalemrot  40451  dalem10  40467  arglem1N  40984  cdlemk36  41707  resopunitintvd  42813  resclunitintvd  42814  lcmineqlem2  42817  aks6d1c7lem1  42967  aks5lem2  42974  mzpconstmpt  43491  mzpresrename  43501  diophrex  43526  0dioph  43529  anrabdioph  43531  orrabdioph  43532  rabren3dioph  43562  dvradcnv2  45077  xpexb  45182  fsumcnf  45761  uzublem  46164  fprodcncf  46634  iblconstmpt  46690  itgiccshift  46714  itgperiod  46715  itgsbtaddcnst  46716  dirkercncflem2  46838  fourierdlem47  46887  saluni  47059  sge0iunmpt  47152  sge0xaddlem2  47168  sge0xadd  47169  hoicvr  47282  hoidmvlelem3  47331  ctvonmbl  47423  vonct  47427  smfaddlem2  47498  smfmullem4  47528  aoprssdm  47959  rescofuf  49891  idfu1stalem  49898  idfu1sta  49899  idfu1a  49900  idfu2nda  49901  oppfuprcl  50002  lmddu  50465  cmddu  50466