Theorem eleqtrrdi 2325

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 2235	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2324	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  brelrng  4963  elabrex  5897  elabrexg  5898  fliftel1  5934  ovidig  6138  unielxp  6336  2oconcl  6606  ecopqsi  6758  eroprf  6796  exmidpweq  7100  sbthlem2  7156  djulclr  7247  djurclr  7248  djulcl  7249  djurcl  7250  caseinl  7289  caseinr  7290  ctssdccl  7309  isnumi  7385  addclnq  7594  mulclnq  7595  recexnq  7609  ltexnqq  7627  prarloclemarch  7637  prarloclemarch2  7638  nnnq  7641  nqnq0  7660  addclnq0  7670  mulclnq0  7671  nqpnq0nq  7672  prarloclemlt  7712  prarloclemlo  7713  prarloclemcalc  7721  nqprm  7761  cauappcvgprlem2  7879  caucvgprlem2  7899  addclsr  7972  mulclsr  7973  prsrcl  8003  mappsrprg  8023  suplocsrlemb  8025  pitonnlem2  8066  pitore  8069  recnnre  8070  axaddcl  8083  axmulcl  8085  axcaucvglemcl  8114  axcaucvglemval  8116  axcaucvglemcau  8117  axcaucvglemres  8118  uztrn2  9773  eluz2nn  9799  peano2uzs  9817  rebtwn2z  10513  seqf  10725  ser0  10794  bcm1k  11021  bcp1nk  11023  bcpasc  11027  hashennn  11041  hashcl  11042  climconst  11850  climshft2  11866  clim2ser  11897  clim2ser2  11898  iserex  11899  serf0  11912  zsumdc  11944  fsump1i  11993  iserabs  12035  isumshft  12050  isumsplit  12051  isum1p  12052  isumrpcl  12054  cvgratnnlemseq  12086  cvgratz  12092  cvgratgt0  12093  clim2prod  12099  clim2divap  12100  prodf1  12102  ntrivcvgap0  12109  zproddc  12139  fprodntrivap  12144  fprodabs  12176  fprodeq0  12177  ef0lem  12220  dvdsflip  12411  fzo0dvdseq  12417  bitsinv1  12522  gcdsupcl  12528  nninfctlemfo  12610  ialgr0  12615  prmind2  12691  crth  12795  prmdiv  12806  pockthlem  12928  pockthg  12929  prmunb  12934  ennnfonelemkh  13032  ennnfonelemrn  13039  ennnfonelemdm  13040  ctiunctlemf  13058  strslfv2d  13124  bassetsnn  13138  1strbas  13199  2strbasg  13202  2stropg  13203  2strbas1g  13205  rngbaseg  13218  rngplusgg  13219  rngmulrg  13220  srngbased  13229  srngplusgd  13230  srngmulrd  13231  srnginvld  13232  lmodbased  13247  lmodplusgd  13248  lmodscad  13249  lmodvscad  13250  ipsbased  13259  ipsaddgd  13260  ipsmulrd  13261  ipsscad  13262  ipsvscad  13263  ipsipd  13264  topgrpbasd  13279  topgrpplusgd  13280  topgrptsetd  13281  mulgnnp1  13716  znf1o  14664  lmconst  14939  lmss  14969  uptx  14997  cnmpt1res  15019  dvidlemap  15414  dvidrelem  15415  dvrecap  15436  plycolemc  15481  plycn  15485  pilem3  15506  logbleb  15684  logblt  15685  lgseisenlem1  15798  structvtxval  15889  ushgredgedgloop  16078  subgruhgredgdm  16120  wlkvtxm  16190  wlk1walkdom  16209  djulclALT  16397  djurclALT  16398  pwle2  16599  trilpolemeq1  16644