Theorem eleqtrrdi 2299

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  brelrng  4909  elabrex  5826  elabrexg  5827  fliftel1  5863  ovidig  6063  unielxp  6260  2oconcl  6525  ecopqsi  6677  eroprf  6715  exmidpweq  7006  sbthlem2  7060  djulclr  7151  djurclr  7152  djulcl  7153  djurcl  7154  caseinl  7193  caseinr  7194  ctssdccl  7213  isnumi  7289  addclnq  7488  mulclnq  7489  recexnq  7503  ltexnqq  7521  prarloclemarch  7531  prarloclemarch2  7532  nnnq  7535  nqnq0  7554  addclnq0  7564  mulclnq0  7565  nqpnq0nq  7566  prarloclemlt  7606  prarloclemlo  7607  prarloclemcalc  7615  nqprm  7655  cauappcvgprlem2  7773  caucvgprlem2  7793  addclsr  7866  mulclsr  7867  prsrcl  7897  mappsrprg  7917  suplocsrlemb  7919  pitonnlem2  7960  pitore  7963  recnnre  7964  axaddcl  7977  axmulcl  7979  axcaucvglemcl  8008  axcaucvglemval  8010  axcaucvglemcau  8011  axcaucvglemres  8012  uztrn2  9666  eluz2nn  9687  peano2uzs  9705  rebtwn2z  10397  seqf  10609  ser0  10678  bcm1k  10905  bcp1nk  10907  bcpasc  10911  hashennn  10925  hashcl  10926  climconst  11601  climshft2  11617  clim2ser  11648  clim2ser2  11649  iserex  11650  serf0  11663  zsumdc  11695  fsump1i  11744  iserabs  11786  isumshft  11801  isumsplit  11802  isum1p  11803  isumrpcl  11805  cvgratnnlemseq  11837  cvgratz  11843  cvgratgt0  11844  clim2prod  11850  clim2divap  11851  prodf1  11853  ntrivcvgap0  11860  zproddc  11890  fprodntrivap  11895  fprodabs  11927  fprodeq0  11928  ef0lem  11971  dvdsflip  12162  fzo0dvdseq  12168  bitsinv1  12273  gcdsupcl  12279  nninfctlemfo  12361  ialgr0  12366  prmind2  12442  crth  12546  prmdiv  12557  pockthlem  12679  pockthg  12680  prmunb  12685  ennnfonelemkh  12783  ennnfonelemrn  12790  ennnfonelemdm  12791  ctiunctlemf  12809  strslfv2d  12875  1strbas  12949  2strbasg  12952  2stropg  12953  2strbas1g  12955  rngbaseg  12968  rngplusgg  12969  rngmulrg  12970  srngbased  12979  srngplusgd  12980  srngmulrd  12981  srnginvld  12982  lmodbased  12997  lmodplusgd  12998  lmodscad  12999  lmodvscad  13000  ipsbased  13009  ipsaddgd  13010  ipsmulrd  13011  ipsscad  13012  ipsvscad  13013  ipsipd  13014  topgrpbasd  13029  topgrpplusgd  13030  topgrptsetd  13031  mulgnnp1  13466  znf1o  14413  lmconst  14688  lmss  14718  uptx  14746  cnmpt1res  14768  dvidlemap  15163  dvidrelem  15164  dvrecap  15185  plycolemc  15230  plycn  15234  pilem3  15255  logbleb  15433  logblt  15434  lgseisenlem1  15547  structvtxval  15636  djulclALT  15737  djurclALT  15738  pwle2  15935  trilpolemeq1  15979