Theorem eleqtrrdi 2281

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

Syntax hints:   → wi 4   = wceq 1363   ∈ wcel 2158

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183

This theorem is referenced by:  brelrng  4870  elabrex  5771  elabrexg  5772  fliftel1  5808  ovidig  6005  unielxp  6188  2oconcl  6453  ecopqsi  6603  eroprf  6641  exmidpweq  6922  sbthlem2  6970  djulclr  7061  djurclr  7062  djulcl  7063  djurcl  7064  caseinl  7103  caseinr  7104  ctssdccl  7123  isnumi  7194  addclnq  7387  mulclnq  7388  recexnq  7402  ltexnqq  7420  prarloclemarch  7430  prarloclemarch2  7431  nnnq  7434  nqnq0  7453  addclnq0  7463  mulclnq0  7464  nqpnq0nq  7465  prarloclemlt  7505  prarloclemlo  7506  prarloclemcalc  7514  nqprm  7554  cauappcvgprlem2  7672  caucvgprlem2  7692  addclsr  7765  mulclsr  7766  prsrcl  7796  mappsrprg  7816  suplocsrlemb  7818  pitonnlem2  7859  pitore  7862  recnnre  7863  axaddcl  7876  axmulcl  7878  axcaucvglemcl  7907  axcaucvglemval  7909  axcaucvglemcau  7910  axcaucvglemres  7911  uztrn2  9558  eluz2nn  9579  peano2uzs  9597  rebtwn2z  10268  seqf  10474  ser0  10527  bcm1k  10753  bcp1nk  10755  bcpasc  10759  hashennn  10773  hashcl  10774  climconst  11311  climshft2  11327  clim2ser  11358  clim2ser2  11359  iserex  11360  serf0  11373  zsumdc  11405  fsump1i  11454  iserabs  11496  isumshft  11511  isumsplit  11512  isum1p  11513  isumrpcl  11515  cvgratnnlemseq  11547  cvgratz  11553  cvgratgt0  11554  clim2prod  11560  clim2divap  11561  prodf1  11563  ntrivcvgap0  11570  zproddc  11600  fprodntrivap  11605  fprodabs  11637  fprodeq0  11638  ef0lem  11681  dvdsflip  11870  fzo0dvdseq  11876  gcdsupcl  11972  ialgr0  12057  prmind2  12133  crth  12237  prmdiv  12248  pockthlem  12367  pockthg  12368  prmunb  12373  ennnfonelemkh  12426  ennnfonelemrn  12433  ennnfonelemdm  12434  ctiunctlemf  12452  strslfv2d  12518  1strbas  12590  2strbasg  12592  2stropg  12593  2strbas1g  12595  rngbaseg  12608  rngplusgg  12609  rngmulrg  12610  srngbased  12619  srngplusgd  12620  srngmulrd  12621  srnginvld  12622  lmodbased  12637  lmodplusgd  12638  lmodscad  12639  lmodvscad  12640  ipsbased  12649  ipsaddgd  12650  ipsmulrd  12651  ipsscad  12652  ipsvscad  12653  ipsipd  12654  topgrpbasd  12669  topgrpplusgd  12670  topgrptsetd  12671  mulgnnp1  13022  lmconst  13987  lmss  14017  uptx  14045  cnmpt1res  14067  dvidlemap  14431  dvrecap  14448  pilem3  14475  logbleb  14650  logblt  14651  lgseisenlem1  14721  djulclALT  14824  djurclALT  14825  pwle2  15020  trilpolemeq1  15060