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  4961  elabrex  5893  elabrexg  5894  fliftel1  5930  ovidig  6134  unielxp  6332  2oconcl  6602  ecopqsi  6754  eroprf  6792  exmidpweq  7094  sbthlem2  7148  djulclr  7239  djurclr  7240  djulcl  7241  djurcl  7242  caseinl  7281  caseinr  7282  ctssdccl  7301  isnumi  7377  addclnq  7585  mulclnq  7586  recexnq  7600  ltexnqq  7618  prarloclemarch  7628  prarloclemarch2  7629  nnnq  7632  nqnq0  7651  addclnq0  7661  mulclnq0  7662  nqpnq0nq  7663  prarloclemlt  7703  prarloclemlo  7704  prarloclemcalc  7712  nqprm  7752  cauappcvgprlem2  7870  caucvgprlem2  7890  addclsr  7963  mulclsr  7964  prsrcl  7994  mappsrprg  8014  suplocsrlemb  8016  pitonnlem2  8057  pitore  8060  recnnre  8061  axaddcl  8074  axmulcl  8076  axcaucvglemcl  8105  axcaucvglemval  8107  axcaucvglemcau  8108  axcaucvglemres  8109  uztrn2  9764  eluz2nn  9790  peano2uzs  9808  rebtwn2z  10504  seqf  10716  ser0  10785  bcm1k  11012  bcp1nk  11014  bcpasc  11018  hashennn  11032  hashcl  11033  climconst  11841  climshft2  11857  clim2ser  11888  clim2ser2  11889  iserex  11890  serf0  11903  zsumdc  11935  fsump1i  11984  iserabs  12026  isumshft  12041  isumsplit  12042  isum1p  12043  isumrpcl  12045  cvgratnnlemseq  12077  cvgratz  12083  cvgratgt0  12084  clim2prod  12090  clim2divap  12091  prodf1  12093  ntrivcvgap0  12100  zproddc  12130  fprodntrivap  12135  fprodabs  12167  fprodeq0  12168  ef0lem  12211  dvdsflip  12402  fzo0dvdseq  12408  bitsinv1  12513  gcdsupcl  12519  nninfctlemfo  12601  ialgr0  12606  prmind2  12682  crth  12786  prmdiv  12797  pockthlem  12919  pockthg  12920  prmunb  12925  ennnfonelemkh  13023  ennnfonelemrn  13030  ennnfonelemdm  13031  ctiunctlemf  13049  strslfv2d  13115  bassetsnn  13129  1strbas  13190  2strbasg  13193  2stropg  13194  2strbas1g  13196  rngbaseg  13209  rngplusgg  13210  rngmulrg  13211  srngbased  13220  srngplusgd  13221  srngmulrd  13222  srnginvld  13223  lmodbased  13238  lmodplusgd  13239  lmodscad  13240  lmodvscad  13241  ipsbased  13250  ipsaddgd  13251  ipsmulrd  13252  ipsscad  13253  ipsvscad  13254  ipsipd  13255  topgrpbasd  13270  topgrpplusgd  13271  topgrptsetd  13272  mulgnnp1  13707  znf1o  14655  lmconst  14930  lmss  14960  uptx  14988  cnmpt1res  15010  dvidlemap  15405  dvidrelem  15406  dvrecap  15427  plycolemc  15472  plycn  15476  pilem3  15497  logbleb  15675  logblt  15676  lgseisenlem1  15789  structvtxval  15880  ushgredgedgloop  16067  wlkvtxm  16137  wlk1walkdom  16156  djulclALT  16333  djurclALT  16334  pwle2  16535  trilpolemeq1  16580