Theorem eleqtrrdi 2260

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

Syntax hints:   → wi 4   = wceq 1343   ∈ wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  brelrng  4835  elabrex  5726  fliftel1  5762  ovidig  5959  unielxp  6142  2oconcl  6407  ecopqsi  6556  eroprf  6594  exmidpweq  6875  sbthlem2  6923  djulclr  7014  djurclr  7015  djulcl  7016  djurcl  7017  caseinl  7056  caseinr  7057  ctssdccl  7076  isnumi  7138  addclnq  7316  mulclnq  7317  recexnq  7331  ltexnqq  7349  prarloclemarch  7359  prarloclemarch2  7360  nnnq  7363  nqnq0  7382  addclnq0  7392  mulclnq0  7393  nqpnq0nq  7394  prarloclemlt  7434  prarloclemlo  7435  prarloclemcalc  7443  nqprm  7483  cauappcvgprlem2  7601  caucvgprlem2  7621  addclsr  7694  mulclsr  7695  prsrcl  7725  mappsrprg  7745  suplocsrlemb  7747  pitonnlem2  7788  pitore  7791  recnnre  7792  axaddcl  7805  axmulcl  7807  axcaucvglemcl  7836  axcaucvglemval  7838  axcaucvglemcau  7839  axcaucvglemres  7840  uztrn2  9483  eluz2nn  9504  peano2uzs  9522  rebtwn2z  10190  seqf  10396  ser0  10449  bcm1k  10673  bcp1nk  10675  bcpasc  10679  hashennn  10693  hashcl  10694  climconst  11231  climshft2  11247  clim2ser  11278  clim2ser2  11279  iserex  11280  serf0  11293  zsumdc  11325  fsump1i  11374  iserabs  11416  isumshft  11431  isumsplit  11432  isum1p  11433  isumrpcl  11435  cvgratnnlemseq  11467  cvgratz  11473  cvgratgt0  11474  clim2prod  11480  clim2divap  11481  prodf1  11483  ntrivcvgap0  11490  zproddc  11520  fprodntrivap  11525  fprodabs  11557  fprodeq0  11558  ef0lem  11601  dvdsflip  11789  fzo0dvdseq  11795  gcdsupcl  11891  ialgr0  11976  prmind2  12052  crth  12156  prmdiv  12167  pockthlem  12286  pockthg  12287  prmunb  12292  ennnfonelemkh  12345  ennnfonelemrn  12352  ennnfonelemdm  12353  ctiunctlemf  12371  strslfv2d  12436  1strbas  12494  2strbasg  12496  2stropg  12497  2strbas1g  12499  rngbaseg  12511  rngplusgg  12512  rngmulrg  12513  srngbased  12518  srngplusgd  12519  srngmulrd  12520  srnginvld  12521  lmodbased  12529  lmodplusgd  12530  lmodscad  12531  lmodvscad  12532  ipsbased  12537  ipsaddgd  12538  ipsmulrd  12539  ipsscad  12540  ipsvscad  12541  ipsipd  12542  topgrpbasd  12547  topgrpplusgd  12548  topgrptsetd  12549  lmconst  12856  lmss  12886  uptx  12914  cnmpt1res  12936  dvidlemap  13300  dvrecap  13317  pilem3  13344  logbleb  13519  logblt  13520  djulclALT  13682  djurclALT  13683  pwle2  13878  trilpolemeq1  13919