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 1561   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755  df-clel 2838

This theorem is referenced by:  3eltr3g  2879  dmrnssfld  5951  oprssdm  7578  offval  7670  pwexr  7749  cnvexg  7906  resfunexgALT  7930  abrexex2g  7946  opabex3d  7947  opabex3rd  7948  frxp3  8132  suppssov1  8178  suppssov2  8179  suppssfv  8183  ralxpmap  8879  unfi  9140  imafi  9260  pwfir  9262  pwfilem  9263  resfnfinfin  9281  residfi  9282  abrexfi  9296  ssfii  9366  wdomima2g  9535  unxpwdom2  9537  tskwe  9909  ac10ct  9991  fin23lem28  10298  fin23lem30  10300  axcclem  10415  distrlem4pr  10985  iccshftr  13491  iccshftl  13493  iccdil  13495  icccntr  13497  o1res  15588  exprmfct  16740  infpnlem1  16947  4sqlem13  16994  0ram  17057  ressval3d  17283  ismred2  17632  mreexexlem2d  17678  mreexexlem4d  17680  acsfn1c  17695  acsfn2  17696  ssclem  17853  submacs  18862  symgtset  19440  symgsubmefmndALT  19444  efgrcl  19756  cntrcmnd  19883  cntrabl  19884  dprd2da  20085  ogrpaddltrbid  20182  srgbinom  20282  irredlmul  20478  rngridlmcl  21288  lidlrsppropd  21315  rngqiprngghmlem1  21358  rngqiprnglinlem2  21363  rngqiprngimf1lem  21365  rngqiprng  21367  rngqiprngimf  21368  rngqiprngghm  21370  rngqiprngimf1  21371  rngqiprngimfo  21372  rng2idl1cntr  21376  rngqiprngfulem4  21385  rngqipring1  21387  pzriprnglem6  21539  chrcl  21577  css1  21743  issubassa  21920  ply1crng  22261  ply1ring  22310  ply1lmod  22314  oftpos  22513  tposmap  22518  0opn  22965  fctop2  23066  difopn  23095  tgrest  23220  ordtbas2  23252  ordtopn3  23257  ordtcld3  23260  t1ficld  23388  resthauslem  23424  kgentopon  23599  txbasex  23627  txcnpi  23669  txdis1cn  23696  pthaus  23699  txkgen  23713  cnmptid  23722  cnmptc  23723  cnmpt1st  23729  cnmpt2nd  23730  cnmpt2c  23731  cnmptkc  23740  txconn  23750  hmeoima  23826  hmeocld  23828  xkohmeo  23876  filufint  23981  fin1aufil  23993  flftg  24057  ptcmplem2  24114  tmdmulg  24153  tmdgsum2  24157  submtmd  24165  symgtgp  24167  ghmcnp  24176  qustgpopn  24181  qustgplem  24182  ust0  24281  nrginvrcn  24753  fsumcn  24933  fsum2cn  24934  expcn  24935  cnheibor  25018  evth2  25023  csscld  25312  clsocv  25313  ovoliun2  25569  volfiniun  25610  dyadmbl  25663  mbfeqalem2  25705  mbfss  25709  ismbf3d  25717  mbfadd  25724  i1f0rn  25745  mbfmul  25789  itg2seq  25805  itg2monolem2  25814  itg2monolem3  25815  itg2mono  25816  itgreval  25860  itgge0  25874  itgss3  25878  iblconst  25881  itgconst  25882  ibladdlem  25883  itgfsum  25890  iblabslem  25891  itgabs  25898  cmvth  26054  lhop1lem  26076  dvfsumle  26084  dvfsumlem2  26090  ftc1lem4  26102  itgparts  26110  itgsubstlem  26111  itgsubst  26112  plydivlem1  26358  aannenlem1  26393  taylply2  26432  itgulm  26472  cxpcn  26811  resqrtcn  26815  basellem1  27146  mulogsumlem  27596  mulog2sumlem2  27600  selberg2lem  27615  pntrsumo1  27630  addsuniflem  28095  sltmuls1  28241  sltmuls2  28242  precsexlem11  28311  usgrnbcnvfv  29567  ewlksfval  29803  crctcshwlkn0  30022  pjssmii  31885  rabrexfi  32706  abrexexd  32709  mptiffisupp  32896  pfxlsw2ccat  33129  gsummulsubdishift2s  33252  cntrcrng  33262  dfufd2lem  33746  selvply1rhmlemb  33817  vietalem  33877  ply1degltdimlem  33920  fldgenfldext  33966  fldextrspunlem2  33975  lmatfval  34112  pl1cn  34253  esumcvg  34384  esumcvgsum  34386  sigaval  34409  sigaclfu2  34419  sigapildsys  34460  ldgenpisys  34464  measinb2  34521  braew  34540  unelcarsg  34610  carsgclctunlem2  34617  sibfof  34638  sitgclg  34640  orrvcoel  34764  orrvccel  34765  fsum2dsub  34902  fineqvpow  35412  subfaclefac  35527  cvmsss2  35625  cvmopnlem  35629  satf0suclem  35726  mpstrcl  35892  elmpps  35924  hmeoclda  36694  bj-1uplex  37494  bj-2uplex  37508  icoreclin  37852  broucube  38154  mblfinlem1  38157  cnambfre  38168  ibladdnclem  38176  iblabsnclem  38183  itgabsnc  38189  ftc1cnnclem  38191  ftc1anclem4  38196  ftc1anclem5  38197  ftc1anclem6  38198  ftc1anclem7  38199  ftc2nc  38202  areacirc  38213  zrdivrng  38453  xrnresex  38929  dalemrot  40282  dalem10  40298  arglem1N  40815  cdlemk36  41538  resopunitintvd  42644  resclunitintvd  42645  lcmineqlem2  42648  aks6d1c7lem1  42798  aks5lem2  42805  mzpconstmpt  43322  mzpresrename  43332  diophrex  43357  0dioph  43360  anrabdioph  43362  orrabdioph  43363  rabren3dioph  43393  dvradcnv2  44924  xpexb  45030  fsumcnf  45602  uzublem  46005  fprodcncf  46475  iblconstmpt  46531  itgiccshift  46555  itgperiod  46556  itgsbtaddcnst  46557  dirkercncflem2  46679  fourierdlem47  46728  saluni  46900  sge0iunmpt  46993  sge0xaddlem2  47009  sge0xadd  47010  hoicvr  47123  hoidmvlelem3  47172  ctvonmbl  47264  vonct  47268  smfaddlem2  47339  smfmullem4  47369  aoprssdm  47797  rescofuf  49715  idfu1stalem  49722  idfu1sta  49723  idfu1a  49724  idfu2nda  49725  oppfuprcl  49826  lmddu  50289  cmddu  50290