Theorem eqeltrid 2325

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eqeltrrid  2326  csbexga  4263  rabexd  4283  otexg  4372  tpexg  4592  dmresexg  5088  f1oabexg  5654  funfvex  5715  elfvfvex  5733  riotaexg  6045  riotaeqimp  6066  riotaprop  6067  fnovex  6121  ovexg  6122  elovimad  6132  fovcdm  6235  fnovrn  6240  cofunexg  6342  cofunex2g  6343  abrexex2g  6353  xpexgALT  6370  mpofvex  6445  mptsuppdifd  6499  tfrex  6644  frec0g  6673  freccllem  6678  ecexg  6816  qsexg  6870  pmex  6932  elixpsn  7023  diffifi  7204  unfidisj  7235  prfidisj  7240  tpfidisj  7242  tpfidceq  7243  ssfirab  7250  ssfidc  7251  fnfi  7256  funrnfi  7262  iunfidisj  7266  infclti  7369  supex2g  7379  infex2g  7380  djuex  7389  ctssdccl  7457  addvalex  8217  negcl  8533  intqfrac2  10776  intfracq  10777  frec2uzzd  10857  frecuzrdgrrn  10865  iseqf1olemqpcl  10966  seq3f1olemqsum  10970  seqf1oglem1  10976  seqf1oglem2  10977  bcval5  11222  hashf1lem2  11307  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12  11526  pfxccat3  11527  pfxccatpfx2  11530  pfxccat3a  11531  swrdccat3blem  11532  swrdccat3b  11533  cats1cld  11556  xrmaxiflemval  12040  climmpt  12090  reccn2ap  12103  zsumdc  12175  fsumzcl2  12196  fsump1i  12224  fsumabs  12256  hash2iun1dif1  12271  mertenslemi1  12326  fprodcllemf  12404  bitsfzolem  12745  nninfctlemfo  12841  algrf  12847  algcvg  12850  algcvga  12853  algfx  12854  eucalgcvga  12860  eucalg  12861  crth  13030  phimullem  13031  eulerthlemth  13038  prmdiv  13041  pythagtriplem11  13081  pythagtriplem13  13083  pcprecl  13096  infpnlem1  13166  infpnlem2  13167  4sqlem5  13189  mul4sqlem  13200  4sqlemafi  13202  4sqlem13m  13210  4sqlem14  13211  4sqlem17  13214  4sqlem18  13215  ennnfonelemj0  13349  ennnfonelemom  13356  ressbasid  13482  ressval3d  13484  1strbas  13529  2strbasg  13532  2stropg  13533  restid  13662  topnvalg  13663  topnidg  13664  imasival  13685  imasmulr  13688  imasaddfn  13696  imasaddval  13697  imasaddf  13698  imasmulfn  13699  imasmulval  13700  imasmulf  13701  qusval  13702  qusaddval  13714  qusaddf  13715  qusmulval  13716  qusmulf  13717  plusffvalg  13740  plusfvalg  13741  grpidvalg  13751  gzsumvalx  13767  gzsumfzval  13769  gzsum0  13771  gzsumsplit1r  13773  issubmnd  13813  ress0g  13814  ismhm  13826  0mhm  13851  grpinvfvalg  13905  grpinvval  13906  grpinvfng  13907  grpsubfvalg  13908  grpsubval  13909  grpressid  13924  grplactfval  13964  mulgfvalg  13982  mulgval  13983  mulgfng  13985  mulgnngzsum  13988  mulgnnp1  13991  mulgnndir  14012  issubg  14034  subggrp  14038  issubg2m  14050  eqgfval  14083  eqgen  14088  quselbasg  14091  quseccl0g  14092  isghm  14104  ghmima  14126  cntzex  14149  cntrval  14150  cntzfval  14151  cntzval  14152  cntrnsg  14175  ablressid  14228  gzsumshift  14238  gsumclfi  14248  gsumsubmclfi  14252  gsum2dfilem1  14270  gsum2dfilem2  14271  gsum2d2fi  14273  prdsval  14279  prdsplusg  14283  prdsmulr  14284  prdssgrpd  14297  prdsinvlem  14302  xpsval  14307  pwsval  14310  pwselbasb  14312  pwssnf1o  14317  mgpvalg  14326  mgpplusgg  14327  mgptopng  14334  mgpress  14336  rngressid  14359  issrg  14375  ringidss  14440  ring1  14470  ringressid  14476  opprvalg  14482  opprmulfvalg  14483  rdivmuldivd  14559  isnzr2  14599  issubrg  14637  subrgring  14640  rrgval  14678  islmod  14735  scaffvalg  14751  scafvalg  14752  lsssetm  14801  islssm  14802  islssmg  14803  lss1d  14828  lspfval  14833  lspval  14835  lspcl  14836  ellspsn  14862  rnglidlmmgm  14941  rnglidlmsgrp  14942  2idlval  14947  2idlvalg  14948  qusrhm  14973  zlmval  15070  zlmvscag  15076  znval  15079  znle  15080  znbaslemnn  15082  znbas  15087  znzrhval  15090  znleval  15096  aspval  15123  asclfval  15129  psrval  15160  psrbagmaxlemfi  15180  gsumbagdiagfi  15185  psrass1filem  15186  psrbasg  15187  psrelbas  15188  psrplusgg  15191  psrmulrg  15195  psrlidmfi  15208  psrridmfi  15209  mvrval2  15216  mplvalg  15222  mplbas  15223  mplplusgg  15236  topopn  15251  topcld  15352  uncld  15356  iuncld  15358  unicld  15359  tgrest  15412  restin  15419  cnco  15464  cnrest  15478  cnptoprest2  15483  lmss  15489  txbasval  15510  txcn  15518  cnmpt12f  15529  hmeoco  15559  idhmeo  15560  blres  15677  metrest  15749  qtopbasss  15764  tgqioo  15798  divcnap  15808  fsumcncntop  15810  cncfmet  15835  sub1cncf  15845  sub2cncf  15846  cdivcncfap  15847  cnrehmeocntop  15853  cnplimcim  15910  limccnpcntop  15918  limccnp2lem  15919  limccnp2cntop  15920  dvfvalap  15924  dvidsslem  15936  dvmptfsum  15968  plyid  15989  logfac  16143  fsumdvdsmul  16302  bposlem3  16330  bposlem5  16332  bposlem6  16333  gausslemma2dlem0b  16391  gausslemma2dlem0d  16393  gausslemma2dlem0h  16397  gausslemma2dlem5a  16406  gausslemma2dlem5  16407  gausslemma2dlem6  16408  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  2lgslem2  16433  2sqlem8  16464  struct2slots2dom  16501  structiedg0val  16503  edgstruct  16527  uhgrunop  16550  incistruhgr  16553  upgrunop  16590  umgrunop  16592  usgredg2v  16687  usgriedgdomord  16688  uspgredgdomord  16692  subgruhgredgdm  16733  uhgrspansubgrlem  16739  uhgrspanop  16745  upgrspanop  16746  umgrspanop  16747  usgrspanop  16748  vtxdgfval  16751  wksfval  16785  wlk1walkdom  16822  clwwlkg  16856  trlsegvdeglem3  16925  trlsegvdeglem5  16927  eupthvdres  16938  eupth2lem3fi  16939  eupth2lembfi  16940  bj-snexg  17160  trilpolemcl  17310