Theorem eleqtrrdi 2264

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

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  brelrng  4842  elabrex  5737  fliftel1  5773  ovidig  5970  unielxp  6153  2oconcl  6418  ecopqsi  6568  eroprf  6606  exmidpweq  6887  sbthlem2  6935  djulclr  7026  djurclr  7027  djulcl  7028  djurcl  7029  caseinl  7068  caseinr  7069  ctssdccl  7088  isnumi  7159  addclnq  7337  mulclnq  7338  recexnq  7352  ltexnqq  7370  prarloclemarch  7380  prarloclemarch2  7381  nnnq  7384  nqnq0  7403  addclnq0  7413  mulclnq0  7414  nqpnq0nq  7415  prarloclemlt  7455  prarloclemlo  7456  prarloclemcalc  7464  nqprm  7504  cauappcvgprlem2  7622  caucvgprlem2  7642  addclsr  7715  mulclsr  7716  prsrcl  7746  mappsrprg  7766  suplocsrlemb  7768  pitonnlem2  7809  pitore  7812  recnnre  7813  axaddcl  7826  axmulcl  7828  axcaucvglemcl  7857  axcaucvglemval  7859  axcaucvglemcau  7860  axcaucvglemres  7861  uztrn2  9504  eluz2nn  9525  peano2uzs  9543  rebtwn2z  10211  seqf  10417  ser0  10470  bcm1k  10694  bcp1nk  10696  bcpasc  10700  hashennn  10714  hashcl  10715  climconst  11253  climshft2  11269  clim2ser  11300  clim2ser2  11301  iserex  11302  serf0  11315  zsumdc  11347  fsump1i  11396  iserabs  11438  isumshft  11453  isumsplit  11454  isum1p  11455  isumrpcl  11457  cvgratnnlemseq  11489  cvgratz  11495  cvgratgt0  11496  clim2prod  11502  clim2divap  11503  prodf1  11505  ntrivcvgap0  11512  zproddc  11542  fprodntrivap  11547  fprodabs  11579  fprodeq0  11580  ef0lem  11623  dvdsflip  11811  fzo0dvdseq  11817  gcdsupcl  11913  ialgr0  11998  prmind2  12074  crth  12178  prmdiv  12189  pockthlem  12308  pockthg  12309  prmunb  12314  ennnfonelemkh  12367  ennnfonelemrn  12374  ennnfonelemdm  12375  ctiunctlemf  12393  strslfv2d  12458  1strbas  12517  2strbasg  12519  2stropg  12520  2strbas1g  12522  rngbaseg  12534  rngplusgg  12535  rngmulrg  12536  srngbased  12541  srngplusgd  12542  srngmulrd  12543  srnginvld  12544  lmodbased  12552  lmodplusgd  12553  lmodscad  12554  lmodvscad  12555  ipsbased  12560  ipsaddgd  12561  ipsmulrd  12562  ipsscad  12563  ipsvscad  12564  ipsipd  12565  topgrpbasd  12570  topgrpplusgd  12571  topgrptsetd  12572  lmconst  13010  lmss  13040  uptx  13068  cnmpt1res  13090  dvidlemap  13454  dvrecap  13471  pilem3  13498  logbleb  13673  logblt  13674  djulclALT  13836  djurclALT  13837  pwle2  14031  trilpolemeq1  14072