Theorem eqeltrrid 2869

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 2868	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2839

This theorem is used by:  3eltr3g  2880  dmrnssfld  5961  oprssdm  7612  offval  7712  pwexr  7789  cnvexg  7946  resfunexgALT  7970  abrexex2g  7986  opabex3d  7987  opabex3rd  7988  frxp3  8181  suppssov1  8228  suppssov2  8229  suppssfv  8233  ralxpmap  8938  unfi  9200  imafi  9321  pwfir  9322  pwfilem  9323  resfnfinfin  9340  residfi  9341  abrexfi  9355  ssfii  9424  wdomima2g  9593  unxpwdom2  9595  tskwe  10044  fin23lem28  10431  fin23lem30  10433  axcclem  10548  distrlem4pr  11124  iccshftr  13630  iccshftl  13632  iccdil  13634  icccntr  13636  o1res  15742  exprmfct  16895  infpnlem1  17103  4sqlem13  17150  0ram  17213  ressval3d  17439  ismred2  17788  mreexexlem2d  17834  mreexexlem4d  17836  acsfn1c  17851  acsfn2  17852  ssclem  18009  submacs  19038  symgtset  19628  symgsubmefmndALT  19632  efgrcl  19944  cntrcmnd  20071  cntrabl  20072  dprd2da  20273  ogrpaddltrbid  20370  srgbinom  20472  irredlmul  20673  rngridlmcl  21511  lidlrsppropd  21547  rngqiprngghmlem1  21598  rngqiprnglinlem2  21603  rngqiprngimf1lem  21605  rngqiprng  21607  rngqiprngimf  21608  rngqiprngghm  21610  rngqiprngimf1  21611  rngqiprngimfo  21612  rng2idl1cntr  21616  rngqiprngfulem4  21625  rngqipring1  21627  pzriprnglem6  21807  chrcl  21845  css1  22011  issubassa  22190  ply1crng  22531  ply1ring  22580  ply1lmod  22584  oftpos  22782  tposmap  22787  0opn  23237  fctop2  23338  difopn  23367  tgrest  23492  ordtbas2  23524  ordtopn3  23529  ordtcld3  23532  t1ficld  23660  resthauslem  23696  kgentopon  23872  txbasex  23900  txcnpi  23942  txdis1cn  23969  pthaus  23972  txkgen  23986  cnmptid  23995  cnmptc  23996  cnmpt1st  24002  cnmpt2nd  24003  cnmpt2c  24004  cnmptkc  24013  txconn  24023  hmeoima  24099  hmeocld  24101  xkohmeo  24149  filufint  24254  fin1aufil  24266  flftg  24330  ptcmplem2  24387  tmdmulg  24426  tmdgsum2  24430  submtmd  24438  symgtgp  24440  ghmcnp  24449  qustgpopn  24454  qustgplem  24455  ust0  24554  nrginvrcn  25026  fsumcn  25206  fsum2cn  25207  expcn  25208  cnheibor  25291  evth2  25296  csscld  25585  clsocv  25586  ovoliun2  25842  volfiniun  25883  dyadmbl  25936  mbfeqalem2  25978  mbfss  25982  ismbf3d  25990  mbfadd  25997  i1f0rn  26018  mbfmul  26062  itg2seq  26078  itg2monolem2  26087  itg2monolem3  26088  itg2mono  26089  itgreval  26132  itgge0  26146  itgss3  26150  iblconst  26153  itgconst  26154  ibladdlem  26155  itgfsum  26162  iblabslem  26163  itgabs  26170  cmvth  26326  lhop1lem  26348  dvfsumle  26356  dvfsumlem2  26362  ftc1lem4  26374  itgparts  26382  itgsubstlem  26383  itgsubst  26384  plydivlem1  26629  aannenlem1  26670  taylply2  26710  itgulm  26750  cxpcn  27088  resqrtcn  27092  basellem1  27423  mulogsumlem  27873  mulog2sumlem2  27877  selberg2lem  27892  pntrsumo1  27907  addsuniflem  28402  sltmuls1  28548  sltmuls2  28549  precsexlem11  28618  usgrnbcnvfv  29961  ewlksfval  30197  crctcshwlkn0  30425  pjssmii  32298  rabrexfi  33159  abrexexd  33162  mptiffisupp  33343  pfxlsw2ccat  33569  gsummulsubdishift2s  33688  cntrcrng  33698  dfufd2lem  34137  selvply1rhmlemb  34207  vietalem  34267  ply1degltdimlem  34310  fldgenfldext  34356  fldextrspunlem2  34365  lmatfval  34502  pl1cn  34643  esumcvg  34774  esumcvgsum  34776  sigaval  34799  sigaclfu2  34809  sigapildsys  34851  ldgenpisys  34855  measinb2  34912  braew  34931  unelcarsg  35000  carsgclctunlem2  35007  sibfof  35028  sitgclg  35030  orrvcoel  35154  orrvccel  35155  fsum2dsub  35292  fineqvpow  35857  j00smo  35962  subfaclefac  36065  cvmsss2  36163  cvmopnlem  36167  satf0suclem  36264  mpstrcl  36430  elmpps  36462  hmeoclda  37251  bj-1uplex  38051  bj-2uplex  38065  icoreclin  38423  broucube  38715  mblfinlem1  38718  cnambfre  38729  ibladdnclem  38737  iblabsnclem  38744  itgabsnc  38750  ftc1cnnclem  38752  ftc1anclem4  38757  ftc1anclem5  38758  ftc1anclem6  38759  ftc1anclem7  38760  ftc2nc  38763  areacirc  38774  zrdivrng  39030  xrnresex  39504  dalemrot  40857  dalem10  40873  arglem1N  41390  cdlemk36  42113  resopunitintvd  43219  resclunitintvd  43220  lcmineqlem2  43223  aks6d1c7lem1  43373  aks5lem2  43380  mzpconstmpt  43894  mzpresrename  43904  diophrex  43929  0dioph  43932  anrabdioph  43934  orrabdioph  43935  rabren3dioph  43965  dvradcnv2  45474  xpexb  45578  rnstructfi  46070  fsumcnf  46180  uzublem  46582  fprodcncf  47052  iblconstmpt  47108  itgiccshift  47132  itgperiod  47133  itgsbtaddcnst  47134  dirkercncflem2  47256  fourierdlem47  47305  saluni  47477  sge0iunmpt  47570  sge0xaddlem2  47586  sge0xadd  47587  hoicvr  47700  hoidmvlelem3  47749  ctvonmbl  47841  vonct  47845  smfaddlem2  47916  smfmullem4  47946  aoprssdm  48414  rescofuf  50350  idfu1stalem  50358  idfu1sta  50359  idfu1a  50360  idfu2nda  50361  oppfuprcl  50462  lmddu  50992  cmddu  50993