Theorem eqeltrrid 2842

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728  df-clel 2814

This theorem is referenced by:  3eltr3g  2853  dmrnssfld  5891  oprssdm  7485  offval  7574  pwexr  7647  cnvexg  7803  resfunexgALT  7822  abrexexgOLD  7836  abrexex2g  7839  opabex3d  7840  opabex3rd  7841  suppssov1  8045  suppssfv  8049  ralxpmap  8715  unfi  8993  pwfir  8997  pwfilem  8998  residfi  9144  imafiALT  9156  abrexfi  9163  ssfii  9222  wdomima2g  9389  unxpwdom2  9391  tskwe  9752  ac10ct  9836  fin23lem28  10142  fin23lem30  10144  axcclem  10259  distrlem4pr  10828  iccshftr  13264  iccshftl  13266  iccdil  13268  icccntr  13270  o1res  15314  exprmfct  16454  infpnlem1  16656  4sqlem13  16703  0ram  16766  ressval3d  17001  ressval3dOLD  17002  ismred2  17357  mreexexlem2d  17399  mreexexlem4d  17401  acsfn1c  17416  acsfn2  17417  ssclem  17576  submacs  18510  symgtset  19052  symgsubmefmndALT  19056  efgrcl  19366  cntrcmnd  19488  cntrabl  19489  dprd2da  19690  srgbinom  19826  irredlmul  19995  lidlrsppropd  20546  chrcl  20775  css1  20940  issubassa  21118  ply1crng  21414  ply1ring  21464  ply1lmod  21468  oftpos  21646  tposmap  21651  0opn  22098  fctop2  22200  difopn  22230  tgrest  22355  ordtbas2  22387  ordtopn3  22392  ordtcld3  22395  t1ficld  22523  resthauslem  22559  kgentopon  22734  txbasex  22762  txcnpi  22804  txdis1cn  22831  pthaus  22834  txkgen  22848  cnmptid  22857  cnmptc  22858  cnmpt1st  22864  cnmpt2nd  22865  cnmpt2c  22866  cnmptkc  22875  txconn  22885  hmeoima  22961  hmeocld  22963  xkohmeo  23011  filufint  23116  fin1aufil  23128  flftg  23192  ptcmplem2  23249  tmdmulg  23288  tmdgsum2  23292  submtmd  23300  symgtgp  23302  ghmcnp  23311  qustgpopn  23316  qustgplem  23317  ust0  23416  nrginvrcn  23901  fsumcn  24078  fsum2cn  24079  expcn  24080  cnheibor  24163  evth2  24168  csscld  24458  clsocv  24459  ovoliun2  24715  volfiniun  24756  dyadmbl  24809  mbfeqalem2  24851  mbfss  24855  ismbf3d  24863  mbfadd  24870  i1f0rn  24891  mbfmul  24936  itg2seq  24952  itg2monolem2  24961  itg2monolem3  24962  itg2mono  24963  itgreval  25006  itgge0  25020  itgss3  25024  iblconst  25027  itgconst  25028  ibladdlem  25029  itgfsum  25036  iblabslem  25037  itgabs  25044  lhop1lem  25222  dvfsumle  25230  dvfsumlem2  25236  ftc1lem4  25248  itgparts  25256  itgsubstlem  25257  itgsubst  25258  plydivlem1  25498  aannenlem1  25533  taylply2  25572  itgulm  25612  cxpcn  25943  resqrtcn  25947  basellem1  26275  mulogsumlem  26724  mulog2sumlem2  26728  selberg2lem  26743  pntrsumo1  26758  usgrnbcnvfv  27777  ewlksfval  28013  crctcshwlkn0  28231  pjssmii  30088  abrexexd  30899  pfxlsw2ccat  31269  cntrcrng  31367  ogrpaddltrbid  31391  lmatfval  31809  pl1cn  31950  esumcvg  32099  esumcvgsum  32101  sigaval  32124  sigaclfu2  32134  sigapildsys  32175  ldgenpisys  32179  measinb2  32236  braew  32255  unelcarsg  32324  carsgclctunlem2  32331  sibfof  32352  sitgclg  32354  orrvcoel  32477  orrvccel  32478  fsum2dsub  32632  fineqvpow  33110  subfaclefac  33183  cvmsss2  33281  cvmopnlem  33285  satf0suclem  33382  mpstrcl  33548  elmpps  33580  hmeoclda  34567  bj-1uplex  35242  bj-2uplex  35256  icoreclin  35572  broucube  35855  mblfinlem1  35858  cnambfre  35869  ibladdnclem  35877  iblabsnclem  35884  itgabsnc  35890  ftc1cnnclem  35892  ftc1anclem4  35897  ftc1anclem5  35898  ftc1anclem6  35899  ftc1anclem7  35900  ftc2nc  35903  areacirc  35914  zrdivrng  36155  xrnresex  36574  dalemrot  37713  dalem10  37729  arglem1N  38246  cdlemk36  38969  resopunitintvd  40076  resclunitintvd  40077  lcmineqlem2  40080  mzpconstmpt  40599  mzpresrename  40609  diophrex  40634  0dioph  40637  anrabdioph  40639  orrabdioph  40640  rabren3dioph  40674  iunrelexp0  41348  dvradcnv2  42003  xpexb  42110  fsumcnf  42602  uzublem  43018  fprodcncf  43490  iblconstmpt  43546  itgiccshift  43570  itgperiod  43571  itgsbtaddcnst  43572  dirkercncflem2  43694  fourierdlem47  43743  saluni  43914  sge0iunmpt  44006  sge0xaddlem2  44022  sge0xadd  44023  hoidmvlelem3  44185  ctvonmbl  44277  vonct  44281  smfaddlem2  44352  smfmullem4  44382  aoprssdm  44752  singoutnword  46575