Theorem eqeltrid 2316

Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eqeltrid.1	⊢ 𝐴 = 𝐵
eqeltrid.2	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
eqeltrid	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrid

Step	Hyp	Ref	Expression
1		eqeltrid.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqeltrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrd 2306	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eqeltrrid  2317  csbexga  4215  rabexd  4233  otexg  4320  tpexg  4539  dmresexg  5034  f1oabexg  5592  funfvex  5652  elfvfvex  5669  riotaexg  5970  riotaeqimp  5991  riotaprop  5992  fnovex  6046  ovexg  6047  elovimad  6057  fovcdm  6160  fnovrn  6165  cofunexg  6266  cofunex2g  6267  abrexex2g  6277  xpexgALT  6290  mpofvex  6365  tfrex  6529  frec0g  6558  freccllem  6563  ecexg  6701  qsexg  6755  pmex  6817  elixpsn  6899  diffifi  7076  unfidisj  7107  prfidisj  7112  tpfidisj  7114  tpfidceq  7115  ssfirab  7121  ssfidc  7122  fnfi  7126  funrnfi  7132  iunfidisj  7136  infclti  7213  supex2g  7223  infex2g  7224  djuex  7233  ctssdccl  7301  addvalex  8054  negcl  8369  intqfrac2  10571  intfracq  10572  frec2uzzd  10652  frecuzrdgrrn  10660  iseqf1olemqpcl  10761  seq3f1olemqsum  10765  seqf1oglem1  10771  seqf1oglem2  10772  bcval5  11015  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12  11304  pfxccat3  11305  pfxccatpfx2  11308  pfxccat3a  11309  swrdccat3blem  11310  swrdccat3b  11311  cats1cld  11334  xrmaxiflemval  11801  climmpt  11851  reccn2ap  11864  zsumdc  11935  fsumzcl2  11956  fsump1i  11984  fsumabs  12016  hash2iun1dif1  12031  mertenslemi1  12086  fprodcllemf  12164  bitsfzolem  12505  nninfctlemfo  12601  algrf  12607  algcvg  12610  algcvga  12613  algfx  12614  eucalgcvga  12620  eucalg  12621  crth  12786  phimullem  12787  eulerthlemth  12794  prmdiv  12797  pythagtriplem11  12837  pythagtriplem13  12839  pcprecl  12852  infpnlem1  12922  infpnlem2  12923  4sqlem5  12945  mul4sqlem  12956  4sqlemafi  12958  4sqlem13m  12966  4sqlem14  12967  4sqlem17  12970  4sqlem18  12971  ennnfonelemj0  13012  ennnfonelemom  13019  ressbasid  13143  ressval3d  13145  1strbas  13190  2strbasg  13193  2stropg  13194  restid  13323  topnvalg  13324  topnidg  13325  prdsval  13346  prdsplusg  13350  prdsmulr  13351  pwsval  13364  pwselbasb  13366  pwssnf1o  13371  imasival  13379  imasmulr  13382  imasaddfn  13390  imasaddval  13391  imasaddf  13392  imasmulfn  13393  imasmulval  13394  imasmulf  13395  qusval  13396  qusaddval  13408  qusaddf  13409  qusmulval  13410  qusmulf  13411  xpsval  13425  plusffvalg  13435  plusfvalg  13436  grpidvalg  13446  igsumvalx  13462  gsumfzval  13464  gsum0g  13469  gsumsplit1r  13471  gsumprval  13472  prdssgrpd  13488  issubmnd  13515  ress0g  13516  ismhm  13534  0mhm  13559  grpinvfvalg  13615  grpinvval  13616  grpinvfng  13617  grpsubfvalg  13618  grpsubval  13619  grpressid  13634  grplactfval  13674  prdsinvlem  13681  mulgfvalg  13698  mulgval  13699  mulgfng  13701  mulgnngsum  13704  mulgnnp1  13707  mulgnndir  13728  issubg  13750  subggrp  13754  issubg2m  13766  eqgfval  13799  eqgen  13804  quselbasg  13807  quseccl0g  13808  isghm  13820  ghmima  13842  ablressid  13912  gsumfzmptfidmadd  13916  mgpvalg  13926  mgpplusgg  13927  mgptopng  13932  mgpress  13934  rngressid  13957  issrg  13968  ringidss  14032  ring1  14062  ringressid  14066  opprvalg  14072  opprmulfvalg  14073  rdivmuldivd  14148  isnzr2  14188  issubrg  14225  subrgring  14228  rrgval  14266  islmod  14295  scaffvalg  14310  scafvalg  14311  lsssetm  14360  islssm  14361  islssmg  14362  lss1d  14387  lspfval  14392  lspval  14394  lspcl  14395  ellspsn  14421  rnglidlmmgm  14500  rnglidlmsgrp  14501  2idlval  14506  2idlvalg  14507  qusrhm  14532  zlmval  14631  zlmvscag  14637  znval  14640  znle  14641  znbaslemnn  14643  znbas  14648  znzrhval  14651  znleval  14657  psrval  14670  psrbasg  14678  psrelbas  14679  psrplusgg  14682  mplvalcoe  14694  mplbascoe  14695  mplplusgg  14707  topopn  14722  topcld  14823  uncld  14827  iuncld  14829  unicld  14830  tgrest  14883  restin  14890  cnco  14935  cnrest  14949  cnptoprest2  14954  lmss  14960  txbasval  14981  txcn  14989  cnmpt12f  15000  hmeoco  15030  idhmeo  15031  blres  15148  metrest  15220  qtopbasss  15235  tgqioo  15269  divcnap  15279  fsumcncntop  15281  cncfmet  15306  sub1cncf  15316  sub2cncf  15317  cdivcncfap  15318  cnrehmeocntop  15324  cnplimcim  15381  limccnpcntop  15389  limccnp2lem  15390  limccnp2cntop  15391  dvfvalap  15395  dvidsslem  15407  dvmptfsum  15439  plyid  15460  fsumdvdsmul  15705  gausslemma2dlem0b  15769  gausslemma2dlem0d  15771  gausslemma2dlem0h  15775  gausslemma2dlem5a  15784  gausslemma2dlem5  15785  gausslemma2dlem6  15786  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  2lgslem2  15811  2sqlem8  15842  struct2slots2dom  15879  structiedg0val  15881  edgstruct  15905  uhgrunop  15928  incistruhgr  15931  upgrunop  15966  umgrunop  15968  usgredg2v  16063  usgriedgdomord  16064  uspgredgdomord  16068  vtxdgfval  16094  wksfval  16119  wlk1walkdom  16156  clwwlkg  16188  bj-snexg  16443  trilpolemcl  16577