Theorem eleqtrrdi 2298

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

Syntax hints:   → wi 4   = wceq 1372   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  brelrng  4908  elabrex  5825  elabrexg  5826  fliftel1  5862  ovidig  6062  unielxp  6259  2oconcl  6524  ecopqsi  6676  eroprf  6714  exmidpweq  7005  sbthlem2  7059  djulclr  7150  djurclr  7151  djulcl  7152  djurcl  7153  caseinl  7192  caseinr  7193  ctssdccl  7212  isnumi  7288  addclnq  7487  mulclnq  7488  recexnq  7502  ltexnqq  7520  prarloclemarch  7530  prarloclemarch2  7531  nnnq  7534  nqnq0  7553  addclnq0  7563  mulclnq0  7564  nqpnq0nq  7565  prarloclemlt  7605  prarloclemlo  7606  prarloclemcalc  7614  nqprm  7654  cauappcvgprlem2  7772  caucvgprlem2  7792  addclsr  7865  mulclsr  7866  prsrcl  7896  mappsrprg  7916  suplocsrlemb  7918  pitonnlem2  7959  pitore  7962  recnnre  7963  axaddcl  7976  axmulcl  7978  axcaucvglemcl  8007  axcaucvglemval  8009  axcaucvglemcau  8010  axcaucvglemres  8011  uztrn2  9665  eluz2nn  9686  peano2uzs  9704  rebtwn2z  10395  seqf  10607  ser0  10676  bcm1k  10903  bcp1nk  10905  bcpasc  10909  hashennn  10923  hashcl  10924  climconst  11572  climshft2  11588  clim2ser  11619  clim2ser2  11620  iserex  11621  serf0  11634  zsumdc  11666  fsump1i  11715  iserabs  11757  isumshft  11772  isumsplit  11773  isum1p  11774  isumrpcl  11776  cvgratnnlemseq  11808  cvgratz  11814  cvgratgt0  11815  clim2prod  11821  clim2divap  11822  prodf1  11824  ntrivcvgap0  11831  zproddc  11861  fprodntrivap  11866  fprodabs  11898  fprodeq0  11899  ef0lem  11942  dvdsflip  12133  fzo0dvdseq  12139  bitsinv1  12244  gcdsupcl  12250  nninfctlemfo  12332  ialgr0  12337  prmind2  12413  crth  12517  prmdiv  12528  pockthlem  12650  pockthg  12651  prmunb  12656  ennnfonelemkh  12754  ennnfonelemrn  12761  ennnfonelemdm  12762  ctiunctlemf  12780  strslfv2d  12846  1strbas  12920  2strbasg  12923  2stropg  12924  2strbas1g  12926  rngbaseg  12939  rngplusgg  12940  rngmulrg  12941  srngbased  12950  srngplusgd  12951  srngmulrd  12952  srnginvld  12953  lmodbased  12968  lmodplusgd  12969  lmodscad  12970  lmodvscad  12971  ipsbased  12980  ipsaddgd  12981  ipsmulrd  12982  ipsscad  12983  ipsvscad  12984  ipsipd  12985  topgrpbasd  13000  topgrpplusgd  13001  topgrptsetd  13002  mulgnnp1  13437  znf1o  14384  lmconst  14659  lmss  14689  uptx  14717  cnmpt1res  14739  dvidlemap  15134  dvidrelem  15135  dvrecap  15156  plycolemc  15201  plycn  15205  pilem3  15226  logbleb  15404  logblt  15405  lgseisenlem1  15518  structvtxval  15607  djulclALT  15699  djurclALT  15700  pwle2  15897  trilpolemeq1  15941