Theorem eleqtrrdi 2323

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  brelrng  4955  elabrex  5887  elabrexg  5888  fliftel1  5924  ovidig  6128  unielxp  6326  2oconcl  6593  ecopqsi  6745  eroprf  6783  exmidpweq  7082  sbthlem2  7136  djulclr  7227  djurclr  7228  djulcl  7229  djurcl  7230  caseinl  7269  caseinr  7270  ctssdccl  7289  isnumi  7365  addclnq  7573  mulclnq  7574  recexnq  7588  ltexnqq  7606  prarloclemarch  7616  prarloclemarch2  7617  nnnq  7620  nqnq0  7639  addclnq0  7649  mulclnq0  7650  nqpnq0nq  7651  prarloclemlt  7691  prarloclemlo  7692  prarloclemcalc  7700  nqprm  7740  cauappcvgprlem2  7858  caucvgprlem2  7878  addclsr  7951  mulclsr  7952  prsrcl  7982  mappsrprg  8002  suplocsrlemb  8004  pitonnlem2  8045  pitore  8048  recnnre  8049  axaddcl  8062  axmulcl  8064  axcaucvglemcl  8093  axcaucvglemval  8095  axcaucvglemcau  8096  axcaucvglemres  8097  uztrn2  9752  eluz2nn  9773  peano2uzs  9791  rebtwn2z  10486  seqf  10698  ser0  10767  bcm1k  10994  bcp1nk  10996  bcpasc  11000  hashennn  11014  hashcl  11015  climconst  11816  climshft2  11832  clim2ser  11863  clim2ser2  11864  iserex  11865  serf0  11878  zsumdc  11910  fsump1i  11959  iserabs  12001  isumshft  12016  isumsplit  12017  isum1p  12018  isumrpcl  12020  cvgratnnlemseq  12052  cvgratz  12058  cvgratgt0  12059  clim2prod  12065  clim2divap  12066  prodf1  12068  ntrivcvgap0  12075  zproddc  12105  fprodntrivap  12110  fprodabs  12142  fprodeq0  12143  ef0lem  12186  dvdsflip  12377  fzo0dvdseq  12383  bitsinv1  12488  gcdsupcl  12494  nninfctlemfo  12576  ialgr0  12581  prmind2  12657  crth  12761  prmdiv  12772  pockthlem  12894  pockthg  12895  prmunb  12900  ennnfonelemkh  12998  ennnfonelemrn  13005  ennnfonelemdm  13006  ctiunctlemf  13024  strslfv2d  13090  bassetsnn  13104  1strbas  13165  2strbasg  13168  2stropg  13169  2strbas1g  13171  rngbaseg  13184  rngplusgg  13185  rngmulrg  13186  srngbased  13195  srngplusgd  13196  srngmulrd  13197  srnginvld  13198  lmodbased  13213  lmodplusgd  13214  lmodscad  13215  lmodvscad  13216  ipsbased  13225  ipsaddgd  13226  ipsmulrd  13227  ipsscad  13228  ipsvscad  13229  ipsipd  13230  topgrpbasd  13245  topgrpplusgd  13246  topgrptsetd  13247  mulgnnp1  13682  znf1o  14630  lmconst  14905  lmss  14935  uptx  14963  cnmpt1res  14985  dvidlemap  15380  dvidrelem  15381  dvrecap  15402  plycolemc  15447  plycn  15451  pilem3  15472  logbleb  15650  logblt  15651  lgseisenlem1  15764  structvtxval  15855  ushgredgedgloop  16041  wlkvtxm  16081  wlk1walkdom  16100  djulclALT  16220  djurclALT  16221  pwle2  16423  trilpolemeq1  16468