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  38281  broucube  38573  mblfinlem1  38576  cnambfre  38587  ibladdnclem  38595  iblabsnclem  38602  itgabsnc  38608  ftc1cnnclem  38610  ftc1anclem4  38615  ftc1anclem5  38616  ftc1anclem6  38617  ftc1anclem7  38618  ftc2nc  38621  areacirc  38632  zrdivrng  38888  xrnresex  39362  dalemrot  40715  dalem10  40731  arglem1N  41248  cdlemk36  41971  resopunitintvd  43077  resclunitintvd  43078  lcmineqlem2  43081  aks6d1c7lem1  43231  aks5lem2  43238  mzpconstmpt  43751  mzpresrename  43761  diophrex  43786  0dioph  43789  anrabdioph  43791  orrabdioph  43792  rabren3dioph  43822  dvradcnv2  45331  xpexb  45436  rnstructfi  45928  fsumcnf  46038  uzublem  46440  fprodcncf  46910  iblconstmpt  46966  itgiccshift  46990  itgperiod  46991  itgsbtaddcnst  46992  dirkercncflem2  47114  fourierdlem47  47163  saluni  47335  sge0iunmpt  47428  sge0xaddlem2  47444  sge0xadd  47445  hoicvr  47558  hoidmvlelem3  47607  ctvonmbl  47699  vonct  47703  smfaddlem2  47774  smfmullem4  47804  aoprssdm  48272  rescofuf  50201  idfu1stalem  50208  idfu1sta  50209  idfu1a  50210  idfu2nda  50211  oppfuprcl  50312  lmddu  50775  cmddu  50776