Theorem eqeltrrid 2836

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  3eltr3g  2847  dmrnssfld  5912  oprssdm  7527  offval  7619  pwexr  7698  cnvexg  7854  resfunexgALT  7880  abrexex2g  7896  opabex3d  7897  opabex3rd  7898  frxp3  8081  suppssov1  8127  suppssov2  8128  suppssfv  8132  ralxpmap  8820  unfi  9080  imafi  9199  pwfir  9201  pwfilem  9202  residfi  9222  abrexfi  9236  ssfii  9303  wdomima2g  9472  unxpwdom2  9474  tskwe  9843  ac10ct  9925  fin23lem28  10231  fin23lem30  10233  axcclem  10348  distrlem4pr  10917  iccshftr  13386  iccshftl  13388  iccdil  13390  icccntr  13392  o1res  15467  exprmfct  16615  infpnlem1  16822  4sqlem13  16869  0ram  16932  ressval3d  17157  ismred2  17505  mreexexlem2d  17551  mreexexlem4d  17553  acsfn1c  17568  acsfn2  17569  ssclem  17726  submacs  18735  symgtset  19311  symgsubmefmndALT  19315  efgrcl  19627  cntrcmnd  19754  cntrabl  19755  dprd2da  19956  ogrpaddltrbid  20053  srgbinom  20149  irredlmul  20346  rngridlmcl  21154  lidlrsppropd  21181  rngqiprngghmlem1  21224  rngqiprnglinlem2  21229  rngqiprngimf1lem  21231  rngqiprng  21233  rngqiprngimf  21234  rngqiprngghm  21236  rngqiprngimf1  21237  rngqiprngimfo  21238  rng2idl1cntr  21242  rngqiprngfulem4  21251  rngqipring1  21253  pzriprnglem6  21423  chrcl  21461  css1  21627  issubassa  21804  ply1crng  22111  ply1ring  22160  ply1lmod  22164  oftpos  22367  tposmap  22372  0opn  22819  fctop2  22920  difopn  22949  tgrest  23074  ordtbas2  23106  ordtopn3  23111  ordtcld3  23114  t1ficld  23242  resthauslem  23278  kgentopon  23453  txbasex  23481  txcnpi  23523  txdis1cn  23550  pthaus  23553  txkgen  23567  cnmptid  23576  cnmptc  23577  cnmpt1st  23583  cnmpt2nd  23584  cnmpt2c  23585  cnmptkc  23594  txconn  23604  hmeoima  23680  hmeocld  23682  xkohmeo  23730  filufint  23835  fin1aufil  23847  flftg  23911  ptcmplem2  23968  tmdmulg  24007  tmdgsum2  24011  submtmd  24019  symgtgp  24021  ghmcnp  24030  qustgpopn  24035  qustgplem  24036  ust0  24135  nrginvrcn  24607  fsumcn  24788  fsum2cn  24789  expcn  24790  expcnOLD  24792  cnheibor  24881  evth2  24886  csscld  25176  clsocv  25177  ovoliun2  25434  volfiniun  25475  dyadmbl  25528  mbfeqalem2  25570  mbfss  25574  ismbf3d  25582  mbfadd  25589  i1f0rn  25610  mbfmul  25654  itg2seq  25670  itg2monolem2  25679  itg2monolem3  25680  itg2mono  25681  itgreval  25725  itgge0  25739  itgss3  25743  iblconst  25746  itgconst  25747  ibladdlem  25748  itgfsum  25755  iblabslem  25756  itgabs  25763  cmvth  25922  lhop1lem  25945  dvfsumle  25953  dvfsumleOLD  25954  dvfsumlem2  25960  dvfsumlem2OLD  25961  ftc1lem4  25973  itgparts  25981  itgsubstlem  25982  itgsubst  25983  plydivlem1  26228  aannenlem1  26263  taylply2  26302  taylply2OLD  26303  itgulm  26344  cxpcn  26681  cxpcnOLD  26682  resqrtcn  26686  basellem1  27018  mulogsumlem  27469  mulog2sumlem2  27473  selberg2lem  27488  pntrsumo1  27503  addsuniflem  27944  ssltmul1  28086  ssltmul2  28087  precsexlem11  28155  usgrnbcnvfv  29343  ewlksfval  29580  crctcshwlkn0  29799  pjssmii  31661  rabrexfi  32486  abrexexd  32489  mptiffisupp  32674  pfxlsw2ccat  32931  cntrcrng  33050  dfufd2lem  33514  ply1degltdimlem  33635  fldgenfldext  33681  fldextrspunlem2  33690  lmatfval  33827  pl1cn  33968  esumcvg  34099  esumcvgsum  34101  sigaval  34124  sigaclfu2  34134  sigapildsys  34175  ldgenpisys  34179  measinb2  34236  braew  34255  unelcarsg  34325  carsgclctunlem2  34332  sibfof  34353  sitgclg  34355  orrvcoel  34479  orrvccel  34480  fsum2dsub  34620  fineqvpow  35138  subfaclefac  35220  cvmsss2  35318  cvmopnlem  35322  satf0suclem  35419  mpstrcl  35585  elmpps  35617  hmeoclda  36377  bj-1uplex  37052  bj-2uplex  37066  icoreclin  37401  broucube  37704  mblfinlem1  37707  cnambfre  37718  ibladdnclem  37726  iblabsnclem  37733  itgabsnc  37739  ftc1cnnclem  37741  ftc1anclem4  37746  ftc1anclem5  37747  ftc1anclem6  37748  ftc1anclem7  37749  ftc2nc  37752  areacirc  37763  zrdivrng  38003  xrnresex  38463  dalemrot  39766  dalem10  39782  arglem1N  40299  cdlemk36  41022  resopunitintvd  42129  resclunitintvd  42130  lcmineqlem2  42133  aks6d1c7lem1  42283  aks5lem2  42290  mzpconstmpt  42843  mzpresrename  42853  diophrex  42878  0dioph  42881  anrabdioph  42883  orrabdioph  42884  rabren3dioph  42918  dvradcnv2  44450  xpexb  44556  fsumcnf  45128  uzublem  45538  fprodcncf  46008  iblconstmpt  46064  itgiccshift  46088  itgperiod  46089  itgsbtaddcnst  46090  dirkercncflem2  46212  fourierdlem47  46261  saluni  46433  sge0iunmpt  46526  sge0xaddlem2  46542  sge0xadd  46543  hoidmvlelem3  46705  ctvonmbl  46797  vonct  46801  smfaddlem2  46872  smfmullem4  46902  aoprssdm  47312  rescofuf  49204  idfu1stalem  49211  idfu1sta  49212  idfu1a  49213  idfu2nda  49214  oppfuprcl  49315  lmddu  49778  cmddu  49779