Theorem eqeltrrid 2866

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  3eltr3g  2877  dmrnssfld  5956  oprssdm  7602  offval  7702  pwexr  7779  cnvexg  7936  resfunexgALT  7960  abrexex2g  7976  opabex3d  7977  opabex3rd  7978  frxp3  8168  suppssov1  8214  suppssov2  8215  suppssfv  8219  ralxpmap  8924  unfi  9186  imafi  9307  pwfir  9308  pwfilem  9309  resfnfinfin  9326  residfi  9327  abrexfi  9341  ssfii  9411  wdomima2g  9580  unxpwdom2  9582  tskwe  10031  fin23lem28  10418  fin23lem30  10420  axcclem  10535  distrlem4pr  11111  iccshftr  13617  iccshftl  13619  iccdil  13621  icccntr  13623  o1res  15727  exprmfct  16880  infpnlem1  17088  4sqlem13  17135  0ram  17198  ressval3d  17424  ismred2  17773  mreexexlem2d  17819  mreexexlem4d  17821  acsfn1c  17836  acsfn2  17837  ssclem  17994  submacs  19023  symgtset  19613  symgsubmefmndALT  19617  efgrcl  19929  cntrcmnd  20056  cntrabl  20057  dprd2da  20258  ogrpaddltrbid  20355  srgbinom  20457  irredlmul  20658  rngridlmcl  21496  lidlrsppropd  21532  rngqiprngghmlem1  21583  rngqiprnglinlem2  21588  rngqiprngimf1lem  21590  rngqiprng  21592  rngqiprngimf  21593  rngqiprngghm  21595  rngqiprngimf1  21596  rngqiprngimfo  21597  rng2idl1cntr  21601  rngqiprngfulem4  21610  rngqipring1  21612  pzriprnglem6  21792  chrcl  21830  css1  21996  issubassa  22175  ply1crng  22516  ply1ring  22565  ply1lmod  22569  oftpos  22767  tposmap  22772  0opn  23222  fctop2  23323  difopn  23352  tgrest  23477  ordtbas2  23509  ordtopn3  23514  ordtcld3  23517  t1ficld  23645  resthauslem  23681  kgentopon  23857  txbasex  23885  txcnpi  23927  txdis1cn  23954  pthaus  23957  txkgen  23971  cnmptid  23980  cnmptc  23981  cnmpt1st  23987  cnmpt2nd  23988  cnmpt2c  23989  cnmptkc  23998  txconn  24008  hmeoima  24084  hmeocld  24086  xkohmeo  24134  filufint  24239  fin1aufil  24251  flftg  24315  ptcmplem2  24372  tmdmulg  24411  tmdgsum2  24415  submtmd  24423  symgtgp  24425  ghmcnp  24434  qustgpopn  24439  qustgplem  24440  ust0  24539  nrginvrcn  25011  fsumcn  25191  fsum2cn  25192  expcn  25193  cnheibor  25276  evth2  25281  csscld  25570  clsocv  25571  ovoliun2  25827  volfiniun  25868  dyadmbl  25921  mbfeqalem2  25963  mbfss  25967  ismbf3d  25975  mbfadd  25982  i1f0rn  26003  mbfmul  26047  itg2seq  26063  itg2monolem2  26072  itg2monolem3  26073  itg2mono  26074  itgreval  26117  itgge0  26131  itgss3  26135  iblconst  26138  itgconst  26139  ibladdlem  26140  itgfsum  26147  iblabslem  26148  itgabs  26155  cmvth  26311  lhop1lem  26333  dvfsumle  26341  dvfsumlem2  26347  ftc1lem4  26359  itgparts  26367  itgsubstlem  26368  itgsubst  26369  plydivlem1  26614  aannenlem1  26655  taylply2  26695  itgulm  26735  cxpcn  27073  resqrtcn  27077  basellem1  27408  mulogsumlem  27858  mulog2sumlem2  27862  selberg2lem  27877  pntrsumo1  27892  addsuniflem  28387  sltmuls1  28533  sltmuls2  28534  precsexlem11  28603  usgrnbcnvfv  29946  ewlksfval  30182  crctcshwlkn0  30410  pjssmii  32283  rabrexfi  33102  abrexexd  33105  mptiffisupp  33286  pfxlsw2ccat  33513  gsummulsubdishift2s  33632  cntrcrng  33642  dfufd2lem  34081  selvply1rhmlemb  34151  vietalem  34211  ply1degltdimlem  34254  fldgenfldext  34300  fldextrspunlem2  34309  lmatfval  34446  pl1cn  34587  esumcvg  34718  esumcvgsum  34720  sigaval  34743  sigaclfu2  34753  sigapildsys  34795  ldgenpisys  34799  measinb2  34856  braew  34875  unelcarsg  34944  carsgclctunlem2  34951  sibfof  34972  sitgclg  34974  orrvcoel  35098  orrvccel  35099  fsum2dsub  35236  fineqvpow  35783  subfaclefac  35941  cvmsss2  36039  cvmopnlem  36043  satf0suclem  36140  mpstrcl  36306  elmpps  36338  hmeoclda  37121  bj-1uplex  37921  bj-2uplex  37935  icoreclin  38280  broucube  38572  mblfinlem1  38575  cnambfre  38586  ibladdnclem  38594  iblabsnclem  38601  itgabsnc  38607  ftc1cnnclem  38609  ftc1anclem4  38614  ftc1anclem5  38615  ftc1anclem6  38616  ftc1anclem7  38617  ftc2nc  38620  areacirc  38631  zrdivrng  38887  xrnresex  39361  dalemrot  40714  dalem10  40730  arglem1N  41247  cdlemk36  41970  resopunitintvd  43076  resclunitintvd  43077  lcmineqlem2  43080  aks6d1c7lem1  43230  aks5lem2  43237  mzpconstmpt  43750  mzpresrename  43760  diophrex  43785  0dioph  43788  anrabdioph  43790  orrabdioph  43791  rabren3dioph  43821  dvradcnv2  45330  xpexb  45435  rnstructfi  45927  fsumcnf  46037  uzublem  46439  fprodcncf  46909  iblconstmpt  46965  itgiccshift  46989  itgperiod  46990  itgsbtaddcnst  46991  dirkercncflem2  47113  fourierdlem47  47162  saluni  47334  sge0iunmpt  47427  sge0xaddlem2  47443  sge0xadd  47444  hoicvr  47557  hoidmvlelem3  47606  ctvonmbl  47698  vonct  47702  smfaddlem2  47773  smfmullem4  47803  aoprssdm  48271  rescofuf  50200  idfu1stalem  50207  idfu1sta  50208  idfu1a  50209  idfu2nda  50210  oppfuprcl  50311  lmddu  50774  cmddu  50775