Theorem eqeltrrid 2839

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

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

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 2115  ax-9 2123  ax-ext 2706

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

This theorem is referenced by:  3eltr3g  2850  dmrnssfld  5921  oprssdm  7537  offval  7629  pwexr  7708  cnvexg  7864  resfunexgALT  7890  abrexex2g  7906  opabex3d  7907  opabex3rd  7908  frxp3  8091  suppssov1  8137  suppssov2  8138  suppssfv  8142  ralxpmap  8832  unfi  9093  imafi  9213  pwfir  9215  pwfilem  9216  residfi  9236  abrexfi  9250  ssfii  9320  wdomima2g  9489  unxpwdom2  9491  tskwe  9860  ac10ct  9942  fin23lem28  10248  fin23lem30  10250  axcclem  10365  distrlem4pr  10935  iccshftr  13400  iccshftl  13402  iccdil  13404  icccntr  13406  o1res  15481  exprmfct  16629  infpnlem1  16836  4sqlem13  16883  0ram  16946  ressval3d  17171  ismred2  17520  mreexexlem2d  17566  mreexexlem4d  17568  acsfn1c  17583  acsfn2  17584  ssclem  17741  submacs  18750  symgtset  19326  symgsubmefmndALT  19330  efgrcl  19642  cntrcmnd  19769  cntrabl  19770  dprd2da  19971  ogrpaddltrbid  20068  srgbinom  20164  irredlmul  20362  rngridlmcl  21170  lidlrsppropd  21197  rngqiprngghmlem1  21240  rngqiprnglinlem2  21245  rngqiprngimf1lem  21247  rngqiprng  21249  rngqiprngimf  21250  rngqiprngghm  21252  rngqiprngimf1  21253  rngqiprngimfo  21254  rng2idl1cntr  21258  rngqiprngfulem4  21267  rngqipring1  21269  pzriprnglem6  21439  chrcl  21477  css1  21643  issubassa  21820  ply1crng  22137  ply1ring  22186  ply1lmod  22190  oftpos  22394  tposmap  22399  0opn  22846  fctop2  22947  difopn  22976  tgrest  23101  ordtbas2  23133  ordtopn3  23138  ordtcld3  23141  t1ficld  23269  resthauslem  23305  kgentopon  23480  txbasex  23508  txcnpi  23550  txdis1cn  23577  pthaus  23580  txkgen  23594  cnmptid  23603  cnmptc  23604  cnmpt1st  23610  cnmpt2nd  23611  cnmpt2c  23612  cnmptkc  23621  txconn  23631  hmeoima  23707  hmeocld  23709  xkohmeo  23757  filufint  23862  fin1aufil  23874  flftg  23938  ptcmplem2  23995  tmdmulg  24034  tmdgsum2  24038  submtmd  24046  symgtgp  24048  ghmcnp  24057  qustgpopn  24062  qustgplem  24063  ust0  24162  nrginvrcn  24634  fsumcn  24815  fsum2cn  24816  expcn  24817  expcnOLD  24819  cnheibor  24908  evth2  24913  csscld  25203  clsocv  25204  ovoliun2  25461  volfiniun  25502  dyadmbl  25555  mbfeqalem2  25597  mbfss  25601  ismbf3d  25609  mbfadd  25616  i1f0rn  25637  mbfmul  25681  itg2seq  25697  itg2monolem2  25706  itg2monolem3  25707  itg2mono  25708  itgreval  25752  itgge0  25766  itgss3  25770  iblconst  25773  itgconst  25774  ibladdlem  25775  itgfsum  25782  iblabslem  25783  itgabs  25790  cmvth  25949  lhop1lem  25972  dvfsumle  25980  dvfsumleOLD  25981  dvfsumlem2  25987  dvfsumlem2OLD  25988  ftc1lem4  26000  itgparts  26008  itgsubstlem  26009  itgsubst  26010  plydivlem1  26255  aannenlem1  26290  taylply2  26329  taylply2OLD  26330  itgulm  26371  cxpcn  26708  cxpcnOLD  26709  resqrtcn  26713  basellem1  27045  mulogsumlem  27496  mulog2sumlem2  27500  selberg2lem  27515  pntrsumo1  27530  addsuniflem  27971  ssltmul1  28116  ssltmul2  28117  precsexlem11  28185  usgrnbcnvfv  29387  ewlksfval  29624  crctcshwlkn0  29843  pjssmii  31705  rabrexfi  32530  abrexexd  32533  mptiffisupp  32721  pfxlsw2ccat  32981  gsummulsubdishift2s  33103  cntrcrng  33112  dfufd2lem  33579  vietalem  33684  ply1degltdimlem  33728  fldgenfldext  33774  fldextrspunlem2  33783  lmatfval  33920  pl1cn  34061  esumcvg  34192  esumcvgsum  34194  sigaval  34217  sigaclfu2  34227  sigapildsys  34268  ldgenpisys  34272  measinb2  34329  braew  34348  unelcarsg  34418  carsgclctunlem2  34425  sibfof  34446  sitgclg  34448  orrvcoel  34572  orrvccel  34573  fsum2dsub  34713  fineqvpow  35220  subfaclefac  35319  cvmsss2  35417  cvmopnlem  35421  satf0suclem  35518  mpstrcl  35684  elmpps  35716  hmeoclda  36476  bj-1uplex  37152  bj-2uplex  37166  icoreclin  37501  broucube  37794  mblfinlem1  37797  cnambfre  37808  ibladdnclem  37816  iblabsnclem  37823  itgabsnc  37829  ftc1cnnclem  37831  ftc1anclem4  37836  ftc1anclem5  37837  ftc1anclem6  37838  ftc1anclem7  37839  ftc2nc  37842  areacirc  37853  zrdivrng  38093  xrnresex  38553  dalemrot  39856  dalem10  39872  arglem1N  40389  cdlemk36  41112  resopunitintvd  42219  resclunitintvd  42220  lcmineqlem2  42223  aks6d1c7lem1  42373  aks5lem2  42380  mzpconstmpt  42924  mzpresrename  42934  diophrex  42959  0dioph  42962  anrabdioph  42964  orrabdioph  42965  rabren3dioph  42999  dvradcnv2  44530  xpexb  44636  fsumcnf  45208  uzublem  45616  fprodcncf  46086  iblconstmpt  46142  itgiccshift  46166  itgperiod  46167  itgsbtaddcnst  46168  dirkercncflem2  46290  fourierdlem47  46339  saluni  46511  sge0iunmpt  46604  sge0xaddlem2  46620  sge0xadd  46621  hoidmvlelem3  46783  ctvonmbl  46875  vonct  46879  smfaddlem2  46950  smfmullem4  46980  aoprssdm  47390  rescofuf  49280  idfu1stalem  49287  idfu1sta  49288  idfu1a  49289  idfu2nda  49290  oppfuprcl  49391  lmddu  49854  cmddu  49855