Theorem eqeltrrid 2844

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  3eltr3g  2855  dmrnssfld  5917  oprssdm  7538  offval  7630  pwexr  7709  cnvexg  7865  resfunexgALT  7891  abrexex2g  7907  opabex3d  7908  opabex3rd  7909  frxp3  8092  suppssov1  8138  suppssov2  8139  suppssfv  8143  ralxpmap  8835  unfi  9096  imafi  9216  pwfir  9218  pwfilem  9219  residfi  9239  abrexfi  9253  ssfii  9323  wdomima2g  9492  unxpwdom2  9494  tskwe  9866  ac10ct  9948  fin23lem28  10254  fin23lem30  10256  axcclem  10371  distrlem4pr  10941  iccshftr  13431  iccshftl  13433  iccdil  13435  icccntr  13437  o1res  15514  exprmfct  16666  infpnlem1  16873  4sqlem13  16920  0ram  16983  ressval3d  17208  ismred2  17557  mreexexlem2d  17603  mreexexlem4d  17605  acsfn1c  17620  acsfn2  17621  ssclem  17778  submacs  18787  symgtset  19366  symgsubmefmndALT  19370  efgrcl  19682  cntrcmnd  19809  cntrabl  19810  dprd2da  20011  ogrpaddltrbid  20108  srgbinom  20204  irredlmul  20400  rngridlmcl  21211  lidlrsppropd  21238  rngqiprngghmlem1  21281  rngqiprnglinlem2  21286  rngqiprngimf1lem  21288  rngqiprng  21290  rngqiprngimf  21291  rngqiprngghm  21293  rngqiprngimf1  21294  rngqiprngimfo  21295  rng2idl1cntr  21299  rngqiprngfulem4  21308  rngqipring1  21310  pzriprnglem6  21462  chrcl  21500  css1  21666  issubassa  21843  ply1crng  22184  ply1ring  22233  ply1lmod  22237  oftpos  22436  tposmap  22441  0opn  22888  fctop2  22989  difopn  23018  tgrest  23143  ordtbas2  23175  ordtopn3  23180  ordtcld3  23183  t1ficld  23311  resthauslem  23347  kgentopon  23522  txbasex  23550  txcnpi  23592  txdis1cn  23619  pthaus  23622  txkgen  23636  cnmptid  23645  cnmptc  23646  cnmpt1st  23652  cnmpt2nd  23653  cnmpt2c  23654  cnmptkc  23663  txconn  23673  hmeoima  23749  hmeocld  23751  xkohmeo  23799  filufint  23904  fin1aufil  23916  flftg  23980  ptcmplem2  24037  tmdmulg  24076  tmdgsum2  24080  submtmd  24088  symgtgp  24090  ghmcnp  24099  qustgpopn  24104  qustgplem  24105  ust0  24204  nrginvrcn  24676  fsumcn  24856  fsum2cn  24857  expcn  24858  cnheibor  24941  evth2  24946  csscld  25235  clsocv  25236  ovoliun2  25492  volfiniun  25533  dyadmbl  25586  mbfeqalem2  25628  mbfss  25632  ismbf3d  25640  mbfadd  25647  i1f0rn  25668  mbfmul  25712  itg2seq  25728  itg2monolem2  25737  itg2monolem3  25738  itg2mono  25739  itgreval  25783  itgge0  25797  itgss3  25801  iblconst  25804  itgconst  25805  ibladdlem  25806  itgfsum  25813  iblabslem  25814  itgabs  25821  cmvth  25977  lhop1lem  25999  dvfsumle  26007  dvfsumlem2  26013  ftc1lem4  26025  itgparts  26033  itgsubstlem  26034  itgsubst  26035  plydivlem1  26278  aannenlem1  26313  taylply2  26352  itgulm  26392  cxpcn  26728  resqrtcn  26732  basellem1  27063  mulogsumlem  27513  mulog2sumlem2  27517  selberg2lem  27532  pntrsumo1  27547  addsuniflem  28012  sltmuls1  28158  sltmuls2  28159  precsexlem11  28228  usgrnbcnvfv  29453  ewlksfval  29689  crctcshwlkn0  29908  pjssmii  31771  rabrexfi  32595  abrexexd  32598  mptiffisupp  32786  pfxlsw2ccat  33030  gsummulsubdishift2s  33153  cntrcrng  33163  dfufd2lem  33641  selvply1rhmlemb  33712  vietalem  33772  ply1degltdimlem  33815  fldgenfldext  33861  fldextrspunlem2  33870  lmatfval  34007  pl1cn  34148  esumcvg  34279  esumcvgsum  34281  sigaval  34304  sigaclfu2  34314  sigapildsys  34355  ldgenpisys  34359  measinb2  34416  braew  34435  unelcarsg  34505  carsgclctunlem2  34512  sibfof  34533  sitgclg  34535  orrvcoel  34659  orrvccel  34660  fsum2dsub  34800  fineqvpow  35305  subfaclefac  35413  cvmsss2  35511  cvmopnlem  35515  satf0suclem  35612  mpstrcl  35778  elmpps  35810  hmeoclda  36570  bj-1uplex  37370  bj-2uplex  37384  icoreclin  37728  broucube  38030  mblfinlem1  38033  cnambfre  38044  ibladdnclem  38052  iblabsnclem  38059  itgabsnc  38065  ftc1cnnclem  38067  ftc1anclem4  38072  ftc1anclem5  38073  ftc1anclem6  38074  ftc1anclem7  38075  ftc2nc  38078  areacirc  38089  zrdivrng  38329  xrnresex  38805  dalemrot  40158  dalem10  40174  arglem1N  40691  cdlemk36  41414  resopunitintvd  42520  resclunitintvd  42521  lcmineqlem2  42524  aks6d1c7lem1  42674  aks5lem2  42681  mzpconstmpt  43198  mzpresrename  43208  diophrex  43233  0dioph  43236  anrabdioph  43238  orrabdioph  43239  rabren3dioph  43269  dvradcnv2  44800  xpexb  44906  fsumcnf  45478  uzublem  45881  fprodcncf  46351  iblconstmpt  46407  itgiccshift  46431  itgperiod  46432  itgsbtaddcnst  46433  dirkercncflem2  46555  fourierdlem47  46604  saluni  46776  sge0iunmpt  46869  sge0xaddlem2  46885  sge0xadd  46886  hoicvr  46999  hoidmvlelem3  47048  ctvonmbl  47140  vonct  47144  smfaddlem2  47215  smfmullem4  47245  aoprssdm  47673  rescofuf  49591  idfu1stalem  49598  idfu1sta  49599  idfu1a  49600  idfu2nda  49601  oppfuprcl  49702  lmddu  50165  cmddu  50166