Theorem eleqtrrdi 2290

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  brelrng  4897  elabrex  5804  elabrexg  5805  fliftel1  5841  ovidig  6040  unielxp  6232  2oconcl  6497  ecopqsi  6649  eroprf  6687  exmidpweq  6970  sbthlem2  7024  djulclr  7115  djurclr  7116  djulcl  7117  djurcl  7118  caseinl  7157  caseinr  7158  ctssdccl  7177  isnumi  7249  addclnq  7442  mulclnq  7443  recexnq  7457  ltexnqq  7475  prarloclemarch  7485  prarloclemarch2  7486  nnnq  7489  nqnq0  7508  addclnq0  7518  mulclnq0  7519  nqpnq0nq  7520  prarloclemlt  7560  prarloclemlo  7561  prarloclemcalc  7569  nqprm  7609  cauappcvgprlem2  7727  caucvgprlem2  7747  addclsr  7820  mulclsr  7821  prsrcl  7851  mappsrprg  7871  suplocsrlemb  7873  pitonnlem2  7914  pitore  7917  recnnre  7918  axaddcl  7931  axmulcl  7933  axcaucvglemcl  7962  axcaucvglemval  7964  axcaucvglemcau  7965  axcaucvglemres  7966  uztrn2  9619  eluz2nn  9640  peano2uzs  9658  rebtwn2z  10344  seqf  10556  ser0  10625  bcm1k  10852  bcp1nk  10854  bcpasc  10858  hashennn  10872  hashcl  10873  climconst  11455  climshft2  11471  clim2ser  11502  clim2ser2  11503  iserex  11504  serf0  11517  zsumdc  11549  fsump1i  11598  iserabs  11640  isumshft  11655  isumsplit  11656  isum1p  11657  isumrpcl  11659  cvgratnnlemseq  11691  cvgratz  11697  cvgratgt0  11698  clim2prod  11704  clim2divap  11705  prodf1  11707  ntrivcvgap0  11714  zproddc  11744  fprodntrivap  11749  fprodabs  11781  fprodeq0  11782  ef0lem  11825  dvdsflip  12016  fzo0dvdseq  12022  gcdsupcl  12125  nninfctlemfo  12207  ialgr0  12212  prmind2  12288  crth  12392  prmdiv  12403  pockthlem  12525  pockthg  12526  prmunb  12531  ennnfonelemkh  12629  ennnfonelemrn  12636  ennnfonelemdm  12637  ctiunctlemf  12655  strslfv2d  12721  1strbas  12795  2strbasg  12797  2stropg  12798  2strbas1g  12800  rngbaseg  12813  rngplusgg  12814  rngmulrg  12815  srngbased  12824  srngplusgd  12825  srngmulrd  12826  srnginvld  12827  lmodbased  12842  lmodplusgd  12843  lmodscad  12844  lmodvscad  12845  ipsbased  12854  ipsaddgd  12855  ipsmulrd  12856  ipsscad  12857  ipsvscad  12858  ipsipd  12859  topgrpbasd  12874  topgrpplusgd  12875  topgrptsetd  12876  mulgnnp1  13260  znf1o  14207  lmconst  14452  lmss  14482  uptx  14510  cnmpt1res  14532  dvidlemap  14927  dvidrelem  14928  dvrecap  14949  plycolemc  14994  plycn  14998  pilem3  15019  logbleb  15197  logblt  15198  lgseisenlem1  15311  djulclALT  15447  djurclALT  15448  pwle2  15643  trilpolemeq1  15684