Theorem eleqtrrdi 2332

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  brelrng  5013  elabrex  5963  elabrexg  5964  fliftel1  6000  ovidig  6206  unielxp  6408  2oconcl  6712  ecopqsi  6864  eroprf  6902  exmidpweq  7216  sbthlem2  7275  djulclr  7390  djurclr  7391  djulcl  7392  djurcl  7393  caseinl  7432  caseinr  7433  ctssdccl  7452  isnumi  7528  addclnq  7743  mulclnq  7744  recexnq  7758  ltexnqq  7776  prarloclemarch  7786  prarloclemarch2  7787  nnnq  7790  nqnq0  7809  addclnq0  7819  mulclnq0  7820  nqpnq0nq  7821  prarloclemlt  7861  prarloclemlo  7862  prarloclemcalc  7870  nqprm  7910  cauappcvgprlem2  8028  caucvgprlem2  8048  addclsr  8121  mulclsr  8122  prsrcl  8152  mappsrprg  8172  suplocsrlemb  8174  pitonnlem2  8215  pitore  8218  recnnre  8219  axaddcl  8232  axmulcl  8234  axcaucvglemcl  8263  axcaucvglemval  8265  axcaucvglemcau  8266  axcaucvglemres  8267  uztrn2  9950  eluz2nn  9976  peano2uzs  9994  rebtwn2z  10700  seqf  10915  ser0  10984  bcm1k  11213  bcp1nk  11215  bcpasc  11219  hashennn  11234  hashcl  11235  climconst  12074  climshft2  12090  clim2ser  12121  clim2ser2  12122  iserex  12123  serf0  12136  zsumdc  12169  fsump1i  12218  iserabs  12260  isumshft  12275  isumsplit  12276  isum1p  12277  isumrpcl  12279  cvgratnnlemseq  12311  cvgratz  12317  cvgratgt0  12318  clim2prod  12324  clim2divap  12325  prodf1  12327  ntrivcvgap0  12334  zproddc  12364  fprodntrivap  12369  fprodabs  12401  fprodeq0  12402  ef0lem  12445  dvdsflip  12636  fzo0dvdseq  12642  bitsinv1  12747  gcdsupcl  12753  nninfctlemfo  12835  ialgr0  12840  prmind2  12916  crth  13024  prmdiv  13035  pockthlem  13157  pockthg  13158  prmunb  13163  ennnfonelemkh  13354  ennnfonelemrn  13361  ennnfonelemdm  13362  ctiunctlemf  13380  strslfv2d  13446  bassetsnn  13460  1strbas  13522  2strbasg  13525  2stropg  13526  2strbas1g  13528  rngbaseg  13541  rngplusgg  13542  rngmulrg  13543  srngbased  13552  srngplusgd  13553  srngmulrd  13554  srnginvld  13555  lmodbased  13570  lmodplusgd  13571  lmodscad  13572  lmodvscad  13573  ipsbased  13582  ipsaddgd  13583  ipsmulrd  13584  ipsscad  13585  ipsvscad  13586  ipsipd  13587  topgrpbasd  13602  topgrpplusgd  13603  topgrptsetd  13604  mulgnnp1  13984  znf1o  15037  lmconst  15369  lmss  15399  uptx  15427  cnmpt1res  15449  dvidlemap  15844  dvidrelem  15845  dvrecap  15866  plycolemc  15911  plycn  15915  pilem3  15937  logbleb  16119  logblt  16120  ppiqub  16215  chtqub  16218  lgseisenlem1  16311  structvtxval  16402  ushgredgedgloop  16591  subgruhgredgdm  16633  wlkvtxm  16703  wlk1walkdom  16722  depindlem2  16870  djulclALT  16951  djurclALT  16952  pwle2  17150  trilpolemeq1  17211