Theorem eleqtrrdi 2287

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

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

This theorem is referenced by:  brelrng  4894  elabrex  5801  elabrexg  5802  fliftel1  5838  ovidig  6037  unielxp  6229  2oconcl  6494  ecopqsi  6646  eroprf  6684  exmidpweq  6967  sbthlem2  7019  djulclr  7110  djurclr  7111  djulcl  7112  djurcl  7113  caseinl  7152  caseinr  7153  ctssdccl  7172  isnumi  7244  addclnq  7437  mulclnq  7438  recexnq  7452  ltexnqq  7470  prarloclemarch  7480  prarloclemarch2  7481  nnnq  7484  nqnq0  7503  addclnq0  7513  mulclnq0  7514  nqpnq0nq  7515  prarloclemlt  7555  prarloclemlo  7556  prarloclemcalc  7564  nqprm  7604  cauappcvgprlem2  7722  caucvgprlem2  7742  addclsr  7815  mulclsr  7816  prsrcl  7846  mappsrprg  7866  suplocsrlemb  7868  pitonnlem2  7909  pitore  7912  recnnre  7913  axaddcl  7926  axmulcl  7928  axcaucvglemcl  7957  axcaucvglemval  7959  axcaucvglemcau  7960  axcaucvglemres  7961  uztrn2  9613  eluz2nn  9634  peano2uzs  9652  rebtwn2z  10326  seqf  10538  ser0  10607  bcm1k  10834  bcp1nk  10836  bcpasc  10840  hashennn  10854  hashcl  10855  climconst  11436  climshft2  11452  clim2ser  11483  clim2ser2  11484  iserex  11485  serf0  11498  zsumdc  11530  fsump1i  11579  iserabs  11621  isumshft  11636  isumsplit  11637  isum1p  11638  isumrpcl  11640  cvgratnnlemseq  11672  cvgratz  11678  cvgratgt0  11679  clim2prod  11685  clim2divap  11686  prodf1  11688  ntrivcvgap0  11695  zproddc  11725  fprodntrivap  11730  fprodabs  11762  fprodeq0  11763  ef0lem  11806  dvdsflip  11996  fzo0dvdseq  12002  gcdsupcl  12098  nninfctlemfo  12180  ialgr0  12185  prmind2  12261  crth  12365  prmdiv  12376  pockthlem  12497  pockthg  12498  prmunb  12503  ennnfonelemkh  12572  ennnfonelemrn  12579  ennnfonelemdm  12580  ctiunctlemf  12598  strslfv2d  12664  1strbas  12738  2strbasg  12740  2stropg  12741  2strbas1g  12743  rngbaseg  12756  rngplusgg  12757  rngmulrg  12758  srngbased  12767  srngplusgd  12768  srngmulrd  12769  srnginvld  12770  lmodbased  12785  lmodplusgd  12786  lmodscad  12787  lmodvscad  12788  ipsbased  12797  ipsaddgd  12798  ipsmulrd  12799  ipsscad  12800  ipsvscad  12801  ipsipd  12802  topgrpbasd  12817  topgrpplusgd  12818  topgrptsetd  12819  mulgnnp1  13203  znf1o  14150  lmconst  14395  lmss  14425  uptx  14453  cnmpt1res  14475  dvidlemap  14870  dvidrelem  14871  dvrecap  14892  plycolemc  14936  plycn  14940  pilem3  14959  logbleb  15134  logblt  15135  lgseisenlem1  15227  djulclALT  15363  djurclALT  15364  pwle2  15559  trilpolemeq1  15600