Theorem eleqtrrdi 2332

Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)

Hypotheses

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

Assertion

Ref	Expression
eleqtrrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrdi

Step	Hyp	Ref	Expression
1		eleqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2242	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2331	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced by:  brelrng  5008  elabrex  5953  elabrexg  5954  fliftel1  5990  ovidig  6196  unielxp  6398  2oconcl  6702  ecopqsi  6854  eroprf  6892  exmidpweq  7206  sbthlem2  7265  djulclr  7379  djurclr  7380  djulcl  7381  djurcl  7382  caseinl  7421  caseinr  7422  ctssdccl  7441  isnumi  7517  addclnq  7732  mulclnq  7733  recexnq  7747  ltexnqq  7765  prarloclemarch  7775  prarloclemarch2  7776  nnnq  7779  nqnq0  7798  addclnq0  7808  mulclnq0  7809  nqpnq0nq  7810  prarloclemlt  7850  prarloclemlo  7851  prarloclemcalc  7859  nqprm  7899  cauappcvgprlem2  8017  caucvgprlem2  8037  addclsr  8110  mulclsr  8111  prsrcl  8141  mappsrprg  8161  suplocsrlemb  8163  pitonnlem2  8204  pitore  8207  recnnre  8208  axaddcl  8221  axmulcl  8223  axcaucvglemcl  8252  axcaucvglemval  8254  axcaucvglemcau  8255  axcaucvglemres  8256  uztrn2  9919  eluz2nn  9945  peano2uzs  9963  rebtwn2z  10667  seqf  10879  ser0  10948  bcm1k  11176  bcp1nk  11178  bcpasc  11182  hashennn  11197  hashcl  11198  climconst  12034  climshft2  12050  clim2ser  12081  clim2ser2  12082  iserex  12083  serf0  12096  zsumdc  12129  fsump1i  12178  iserabs  12220  isumshft  12235  isumsplit  12236  isum1p  12237  isumrpcl  12239  cvgratnnlemseq  12271  cvgratz  12277  cvgratgt0  12278  clim2prod  12284  clim2divap  12285  prodf1  12287  ntrivcvgap0  12294  zproddc  12324  fprodntrivap  12329  fprodabs  12361  fprodeq0  12362  ef0lem  12405  dvdsflip  12596  fzo0dvdseq  12602  bitsinv1  12707  gcdsupcl  12713  nninfctlemfo  12795  ialgr0  12800  prmind2  12876  crth  12980  prmdiv  12991  pockthlem  13113  pockthg  13114  prmunb  13119  ennnfonelemkh  13281  ennnfonelemrn  13288  ennnfonelemdm  13289  ctiunctlemf  13307  strslfv2d  13373  bassetsnn  13387  1strbas  13448  2strbasg  13451  2stropg  13452  2strbas1g  13454  rngbaseg  13467  rngplusgg  13468  rngmulrg  13469  srngbased  13478  srngplusgd  13479  srngmulrd  13480  srnginvld  13481  lmodbased  13496  lmodplusgd  13497  lmodscad  13498  lmodvscad  13499  ipsbased  13508  ipsaddgd  13509  ipsmulrd  13510  ipsscad  13511  ipsvscad  13512  ipsipd  13513  topgrpbasd  13528  topgrpplusgd  13529  topgrptsetd  13530  mulgnnp1  13910  znf1o  14958  lmconst  15240  lmss  15270  uptx  15298  cnmpt1res  15320  dvidlemap  15715  dvidrelem  15716  dvrecap  15737  plycolemc  15782  plycn  15786  pilem3  15807  logbleb  15986  logblt  15987  lgseisenlem1  16103  structvtxval  16194  ushgredgedgloop  16383  subgruhgredgdm  16425  wlkvtxm  16495  wlk1walkdom  16514  depindlem2  16662  djulclALT  16743  djurclALT  16744  pwle2  16942  trilpolemeq1  16994