Theorem eqeltrrid 2865

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

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

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 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  3eltr3g  2876  dmrnssfld  5958  oprssdm  7596  offval  7688  pwexr  7765  cnvexg  7922  resfunexgALT  7946  abrexex2g  7962  opabex3d  7963  opabex3rd  7964  frxp3  8150  suppssov1  8196  suppssov2  8197  suppssfv  8201  ralxpmap  8906  unfi  9168  imafi  9288  pwfir  9289  pwfilem  9290  resfnfinfin  9307  residfi  9308  abrexfi  9322  ssfii  9392  wdomima2g  9561  unxpwdom2  9563  tskwe  9958  fin23lem28  10345  fin23lem30  10347  axcclem  10462  distrlem4pr  11038  iccshftr  13542  iccshftl  13544  iccdil  13546  icccntr  13548  o1res  15650  exprmfct  16798  infpnlem1  17005  4sqlem13  17052  0ram  17115  ressval3d  17341  ismred2  17690  mreexexlem2d  17736  mreexexlem4d  17738  acsfn1c  17753  acsfn2  17754  ssclem  17911  submacs  18939  symgtset  19529  symgsubmefmndALT  19533  efgrcl  19845  cntrcmnd  19972  cntrabl  19973  dprd2da  20174  ogrpaddltrbid  20271  srgbinom  20373  irredlmul  20572  rngridlmcl  21408  lidlrsppropd  21444  rngqiprngghmlem1  21493  rngqiprnglinlem2  21498  rngqiprngimf1lem  21500  rngqiprng  21502  rngqiprngimf  21503  rngqiprngghm  21505  rngqiprngimf1  21506  rngqiprngimfo  21507  rng2idl1cntr  21511  rngqiprngfulem4  21520  rngqipring1  21522  pzriprnglem6  21702  chrcl  21740  css1  21906  issubassa  22085  ply1crng  22426  ply1ring  22475  ply1lmod  22479  oftpos  22677  tposmap  22682  0opn  23132  fctop2  23233  difopn  23262  tgrest  23387  ordtbas2  23419  ordtopn3  23424  ordtcld3  23427  t1ficld  23555  resthauslem  23591  kgentopon  23767  txbasex  23795  txcnpi  23837  txdis1cn  23864  pthaus  23867  txkgen  23881  cnmptid  23890  cnmptc  23891  cnmpt1st  23897  cnmpt2nd  23898  cnmpt2c  23899  cnmptkc  23908  txconn  23918  hmeoima  23994  hmeocld  23996  xkohmeo  24044  filufint  24149  fin1aufil  24161  flftg  24225  ptcmplem2  24282  tmdmulg  24321  tmdgsum2  24325  submtmd  24333  symgtgp  24335  ghmcnp  24344  qustgpopn  24349  qustgplem  24350  ust0  24449  nrginvrcn  24921  fsumcn  25101  fsum2cn  25102  expcn  25103  cnheibor  25186  evth2  25191  csscld  25480  clsocv  25481  ovoliun2  25737  volfiniun  25778  dyadmbl  25831  mbfeqalem2  25873  mbfss  25877  ismbf3d  25885  mbfadd  25892  i1f0rn  25913  mbfmul  25957  itg2seq  25973  itg2monolem2  25982  itg2monolem3  25983  itg2mono  25984  itgreval  26027  itgge0  26041  itgss3  26045  iblconst  26048  itgconst  26049  ibladdlem  26050  itgfsum  26057  iblabslem  26058  itgabs  26065  cmvth  26221  lhop1lem  26243  dvfsumle  26251  dvfsumlem2  26257  ftc1lem4  26269  itgparts  26277  itgsubstlem  26278  itgsubst  26279  plydivlem1  26526  aannenlem1  26567  taylply2  26607  itgulm  26647  cxpcn  26985  resqrtcn  26989  basellem1  27320  mulogsumlem  27770  mulog2sumlem2  27774  selberg2lem  27789  pntrsumo1  27804  addsuniflem  28269  sltmuls1  28415  sltmuls2  28416  precsexlem11  28485  usgrnbcnvfv  29828  ewlksfval  30064  crctcshwlkn0  30292  pjssmii  32165  rabrexfi  32984  abrexexd  32987  mptiffisupp  33168  pfxlsw2ccat  33395  gsummulsubdishift2s  33514  cntrcrng  33524  dfufd2lem  33962  selvply1rhmlemb  34032  vietalem  34092  ply1degltdimlem  34135  fldgenfldext  34181  fldextrspunlem2  34190  lmatfval  34327  pl1cn  34468  esumcvg  34599  esumcvgsum  34601  sigaval  34624  sigaclfu2  34634  sigapildsys  34676  ldgenpisys  34680  measinb2  34737  braew  34756  unelcarsg  34826  carsgclctunlem2  34833  sibfof  34854  sitgclg  34856  orrvcoel  34980  orrvccel  34981  fsum2dsub  35118  fineqvpow  35644  subfaclefac  35758  cvmsss2  35856  cvmopnlem  35860  satf0suclem  35957  mpstrcl  36123  elmpps  36155  hmeoclda  36955  bj-1uplex  37755  bj-2uplex  37769  icoreclin  38114  broucube  38406  mblfinlem1  38409  cnambfre  38420  ibladdnclem  38428  iblabsnclem  38435  itgabsnc  38441  ftc1cnnclem  38443  ftc1anclem4  38448  ftc1anclem5  38449  ftc1anclem6  38450  ftc1anclem7  38451  ftc2nc  38454  areacirc  38465  zrdivrng  38706  xrnresex  39180  dalemrot  40533  dalem10  40549  arglem1N  41066  cdlemk36  41789  resopunitintvd  42895  resclunitintvd  42896  lcmineqlem2  42899  aks6d1c7lem1  43049  aks5lem2  43056  mzpconstmpt  43588  mzpresrename  43598  diophrex  43623  0dioph  43626  anrabdioph  43628  orrabdioph  43629  rabren3dioph  43659  dvradcnv2  45174  xpexb  45279  fsumcnf  45858  uzublem  46261  fprodcncf  46731  iblconstmpt  46787  itgiccshift  46811  itgperiod  46812  itgsbtaddcnst  46813  dirkercncflem2  46935  fourierdlem47  46984  saluni  47156  sge0iunmpt  47249  sge0xaddlem2  47265  sge0xadd  47266  hoicvr  47379  hoidmvlelem3  47428  ctvonmbl  47520  vonct  47524  smfaddlem2  47595  smfmullem4  47625  aoprssdm  48093  rescofuf  50022  idfu1stalem  50029  idfu1sta  50030  idfu1a  50031  idfu2nda  50032  oppfuprcl  50133  lmddu  50596  cmddu  50597