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  10916  ser0  10985  bcm1k  11214  bcp1nk  11216  bcpasc  11220  hashennn  11235  hashcl  11236  climconst  12075  climshft2  12091  clim2ser  12122  clim2ser2  12123  iserex  12124  serf0  12137  zsumdc  12170  fsump1i  12219  iserabs  12261  isumshft  12276  isumsplit  12277  isum1p  12278  isumrpcl  12280  cvgratnnlemseq  12312  cvgratz  12318  cvgratgt0  12319  clim2prod  12325  clim2divap  12326  prodf1  12328  ntrivcvgap0  12335  zproddc  12365  fprodntrivap  12370  fprodabs  12402  fprodeq0  12403  ef0lem  12446  dvdsflip  12637  fzo0dvdseq  12643  bitsinv1  12748  gcdsupcl  12754  nninfctlemfo  12836  ialgr0  12841  prmind2  12917  crth  13025  prmdiv  13036  pockthlem  13158  pockthg  13159  prmunb  13164  ennnfonelemkh  13355  ennnfonelemrn  13362  ennnfonelemdm  13363  ctiunctlemf  13381  strslfv2d  13447  bassetsnn  13461  1strbas  13524  2strbasg  13527  2stropg  13528  2strbas1g  13530  rngbaseg  13543  rngplusgg  13544  rngmulrg  13545  srngbased  13554  srngplusgd  13555  srngmulrd  13556  srnginvld  13557  lmodbased  13572  lmodplusgd  13573  lmodscad  13574  lmodvscad  13575  ipsbased  13584  ipsaddgd  13585  ipsmulrd  13586  ipsscad  13587  ipsvscad  13588  ipsipd  13589  topgrpbasd  13604  topgrpplusgd  13605  topgrptsetd  13606  mulgnnp1  13986  cntrsubgnsg  14169  znf1o  15070  lmconst  15408  lmss  15438  uptx  15466  cnmpt1res  15488  dvidlemap  15883  dvidrelem  15884  dvrecap  15905  plycolemc  15950  plycn  15954  pilem3  15976  logbleb  16158  logblt  16159  ppiqub  16254  chtqub  16257  lgseisenlem1  16355  structvtxval  16446  ushgredgedgloop  16635  subgruhgredgdm  16677  wlkvtxm  16747  wlk1walkdom  16766  depindlem2  16914  djulclALT  16995  djurclALT  16996  pwle2  17194  trilpolemeq1  17256