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  5898  elabrexg  5899  fliftel1  5935  ovidig  6139  unielxp  6337  2oconcl  6607  ecopqsi  6759  eroprf  6797  exmidpweq  7101  sbthlem2  7157  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  caseinl  7290  caseinr  7291  ctssdccl  7310  isnumi  7386  addclnq  7595  mulclnq  7596  recexnq  7610  ltexnqq  7628  prarloclemarch  7638  prarloclemarch2  7639  nnnq  7642  nqnq0  7661  addclnq0  7671  mulclnq0  7672  nqpnq0nq  7673  prarloclemlt  7713  prarloclemlo  7714  prarloclemcalc  7722  nqprm  7762  cauappcvgprlem2  7880  caucvgprlem2  7900  addclsr  7973  mulclsr  7974  prsrcl  8004  mappsrprg  8024  suplocsrlemb  8026  pitonnlem2  8067  pitore  8070  recnnre  8071  axaddcl  8084  axmulcl  8086  axcaucvglemcl  8115  axcaucvglemval  8117  axcaucvglemcau  8118  axcaucvglemres  8119  uztrn2  9774  eluz2nn  9800  peano2uzs  9818  rebtwn2z  10515  seqf  10727  ser0  10796  bcm1k  11023  bcp1nk  11025  bcpasc  11029  hashennn  11043  hashcl  11044  climconst  11855  climshft2  11871  clim2ser  11902  clim2ser2  11903  iserex  11904  serf0  11917  zsumdc  11950  fsump1i  11999  iserabs  12041  isumshft  12056  isumsplit  12057  isum1p  12058  isumrpcl  12060  cvgratnnlemseq  12092  cvgratz  12098  cvgratgt0  12099  clim2prod  12105  clim2divap  12106  prodf1  12108  ntrivcvgap0  12115  zproddc  12145  fprodntrivap  12150  fprodabs  12182  fprodeq0  12183  ef0lem  12226  dvdsflip  12417  fzo0dvdseq  12423  bitsinv1  12528  gcdsupcl  12534  nninfctlemfo  12616  ialgr0  12621  prmind2  12697  crth  12801  prmdiv  12812  pockthlem  12934  pockthg  12935  prmunb  12940  ennnfonelemkh  13038  ennnfonelemrn  13045  ennnfonelemdm  13046  ctiunctlemf  13064  strslfv2d  13130  bassetsnn  13144  1strbas  13205  2strbasg  13208  2stropg  13209  2strbas1g  13211  rngbaseg  13224  rngplusgg  13225  rngmulrg  13226  srngbased  13235  srngplusgd  13236  srngmulrd  13237  srnginvld  13238  lmodbased  13253  lmodplusgd  13254  lmodscad  13255  lmodvscad  13256  ipsbased  13265  ipsaddgd  13266  ipsmulrd  13267  ipsscad  13268  ipsvscad  13269  ipsipd  13270  topgrpbasd  13285  topgrpplusgd  13286  topgrptsetd  13287  mulgnnp1  13722  znf1o  14671  lmconst  14946  lmss  14976  uptx  15004  cnmpt1res  15026  dvidlemap  15421  dvidrelem  15422  dvrecap  15443  plycolemc  15488  plycn  15492  pilem3  15513  logbleb  15691  logblt  15692  lgseisenlem1  15805  structvtxval  15896  ushgredgedgloop  16085  subgruhgredgdm  16127  wlkvtxm  16197  wlk1walkdom  16216  depindlem2  16352  djulclALT  16423  djurclALT  16424  pwle2  16625  trilpolemeq1  16670