Theorem eqeltrrid 2841

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 2840	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  3eltr3g  2852  dmrnssfld  5929  oprssdm  7548  offval  7640  pwexr  7719  cnvexg  7875  resfunexgALT  7901  abrexex2g  7917  opabex3d  7918  opabex3rd  7919  frxp3  8101  suppssov1  8147  suppssov2  8148  suppssfv  8152  ralxpmap  8844  unfi  9105  imafi  9225  pwfir  9227  pwfilem  9228  residfi  9248  abrexfi  9262  ssfii  9332  wdomima2g  9501  unxpwdom2  9503  tskwe  9874  ac10ct  9956  fin23lem28  10262  fin23lem30  10264  axcclem  10379  distrlem4pr  10949  iccshftr  13439  iccshftl  13441  iccdil  13443  icccntr  13445  o1res  15522  exprmfct  16674  infpnlem1  16881  4sqlem13  16928  0ram  16991  ressval3d  17216  ismred2  17565  mreexexlem2d  17611  mreexexlem4d  17613  acsfn1c  17628  acsfn2  17629  ssclem  17786  submacs  18795  symgtset  19374  symgsubmefmndALT  19378  efgrcl  19690  cntrcmnd  19817  cntrabl  19818  dprd2da  20019  ogrpaddltrbid  20116  srgbinom  20212  irredlmul  20408  rngridlmcl  21215  lidlrsppropd  21242  rngqiprngghmlem1  21285  rngqiprnglinlem2  21290  rngqiprngimf1lem  21292  rngqiprng  21294  rngqiprngimf  21295  rngqiprngghm  21297  rngqiprngimf1  21298  rngqiprngimfo  21299  rng2idl1cntr  21303  rngqiprngfulem4  21312  rngqipring1  21314  pzriprnglem6  21466  chrcl  21504  css1  21670  issubassa  21847  ply1crng  22162  ply1ring  22211  ply1lmod  22215  oftpos  22417  tposmap  22422  0opn  22869  fctop2  22970  difopn  22999  tgrest  23124  ordtbas2  23156  ordtopn3  23161  ordtcld3  23164  t1ficld  23292  resthauslem  23328  kgentopon  23503  txbasex  23531  txcnpi  23573  txdis1cn  23600  pthaus  23603  txkgen  23617  cnmptid  23626  cnmptc  23627  cnmpt1st  23633  cnmpt2nd  23634  cnmpt2c  23635  cnmptkc  23644  txconn  23654  hmeoima  23730  hmeocld  23732  xkohmeo  23780  filufint  23885  fin1aufil  23897  flftg  23961  ptcmplem2  24018  tmdmulg  24057  tmdgsum2  24061  submtmd  24069  symgtgp  24071  ghmcnp  24080  qustgpopn  24085  qustgplem  24086  ust0  24185  nrginvrcn  24657  fsumcn  24837  fsum2cn  24838  expcn  24839  cnheibor  24922  evth2  24927  csscld  25216  clsocv  25217  ovoliun2  25473  volfiniun  25514  dyadmbl  25567  mbfeqalem2  25609  mbfss  25613  ismbf3d  25621  mbfadd  25628  i1f0rn  25649  mbfmul  25693  itg2seq  25709  itg2monolem2  25718  itg2monolem3  25719  itg2mono  25720  itgreval  25764  itgge0  25778  itgss3  25782  iblconst  25785  itgconst  25786  ibladdlem  25787  itgfsum  25794  iblabslem  25795  itgabs  25802  cmvth  25958  lhop1lem  25980  dvfsumle  25988  dvfsumlem2  25994  ftc1lem4  26006  itgparts  26014  itgsubstlem  26015  itgsubst  26016  plydivlem1  26259  aannenlem1  26294  taylply2  26333  itgulm  26373  cxpcn  26709  resqrtcn  26713  basellem1  27044  mulogsumlem  27494  mulog2sumlem2  27498  selberg2lem  27513  pntrsumo1  27528  addsuniflem  27993  sltmuls1  28139  sltmuls2  28140  precsexlem11  28209  usgrnbcnvfv  29434  ewlksfval  29670  crctcshwlkn0  29889  pjssmii  31752  rabrexfi  32576  abrexexd  32579  mptiffisupp  32766  pfxlsw2ccat  33010  gsummulsubdishift2s  33132  cntrcrng  33142  dfufd2lem  33609  vietalem  33723  ply1degltdimlem  33766  fldgenfldext  33812  fldextrspunlem2  33821  lmatfval  33958  pl1cn  34099  esumcvg  34230  esumcvgsum  34232  sigaval  34255  sigaclfu2  34265  sigapildsys  34306  ldgenpisys  34310  measinb2  34367  braew  34386  unelcarsg  34456  carsgclctunlem2  34463  sibfof  34484  sitgclg  34486  orrvcoel  34610  orrvccel  34611  fsum2dsub  34751  fineqvpow  35259  subfaclefac  35358  cvmsss2  35456  cvmopnlem  35460  satf0suclem  35557  mpstrcl  35723  elmpps  35755  hmeoclda  36515  bj-1uplex  37315  bj-2uplex  37329  icoreclin  37673  broucube  37975  mblfinlem1  37978  cnambfre  37989  ibladdnclem  37997  iblabsnclem  38004  itgabsnc  38010  ftc1cnnclem  38012  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc2nc  38023  areacirc  38034  zrdivrng  38274  xrnresex  38750  dalemrot  40103  dalem10  40119  arglem1N  40636  cdlemk36  41359  resopunitintvd  42465  resclunitintvd  42466  lcmineqlem2  42469  aks6d1c7lem1  42619  aks5lem2  42626  mzpconstmpt  43172  mzpresrename  43182  diophrex  43207  0dioph  43210  anrabdioph  43212  orrabdioph  43213  rabren3dioph  43243  dvradcnv2  44774  xpexb  44880  fsumcnf  45452  uzublem  45858  fprodcncf  46328  iblconstmpt  46384  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  dirkercncflem2  46532  fourierdlem47  46581  saluni  46753  sge0iunmpt  46846  sge0xaddlem2  46862  sge0xadd  46863  hoicvr  46976  hoidmvlelem3  47025  ctvonmbl  47117  vonct  47121  smfaddlem2  47192  smfmullem4  47222  aoprssdm  47650  rescofuf  49568  idfu1stalem  49575  idfu1sta  49576  idfu1a  49577  idfu2nda  49578  oppfuprcl  49679  lmddu  50142  cmddu  50143