Theorem syl5eleqr 2865

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
syl5eleqr.1	⊢ 𝐴 ∈ 𝐵
syl5eleqr.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
syl5eleqr	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl5eleqr

Step	Hyp	Ref	Expression
1		syl5eleqr.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		syl5eleqr.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2783	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	syl5eleq 2864	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2769  df-clel 2773

This theorem is referenced by:  rabsnt  4497  onnev  6096  opabiota  6521  canth  6880  onnseq  7724  tfrlem16  7772  oen0  7950  nnawordex  8001  inf0  8815  cantnflt  8866  cnfcom2  8896  cnfcom3lem  8897  cnfcom3  8898  r1ordg  8938  r1val1  8946  rankr1id  9022  acacni  9297  dfacacn  9298  dfac13  9299  cda1dif  9333  ttukeylem5  9670  ttukeylem6  9671  gch2  9832  gch3  9833  gchac  9838  gchina  9856  swrds1  13771  wrdl3s3  14114  sadcp1  15583  lcmfunsnlem2  15759  xpsfrnel2  16611  idfucl  16926  gsumval2  17666  gsumz  17760  frmdmnd  17783  frmd0  17784  efginvrel2  18524  efgcpbl2  18556  pgpfaclem1  18867  lbsexg  19561  zringndrg  20234  frlmlbs  20540  mat0dimscm  20680  mat0scmat  20749  m2detleiblem5  20836  m2detleiblem6  20837  m2detleiblem3  20840  m2detleiblem4  20841  d0mat2pmat  20950  chpmat0d  21046  dfac14  21830  acufl  22129  cnextfvval  22277  cnextcn  22279  minveclem3b  23634  minveclem4a  23636  ovollb2  23693  ovolunlem1a  23700  ovolunlem1  23701  ovoliunlem1  23706  ovoliun2  23710  ioombl1lem4  23765  uniioombllem1  23785  uniioombllem2  23787  uniioombllem6  23792  itg2monolem1  23954  itg2mono  23957  itg2cnlem1  23965  xrlimcnp  25147  efrlim  25148  eengbas  26330  ebtwntg  26331  ecgrtg  26332  elntg  26333  wlkl1loop  26985  elwwlks2ons3im  27334  upgr3v3e3cycl  27583  upgr4cycl4dv4e  27588  2clwwlk2clwwlk  27761  2clwwlk2clwwlkOLD  27762  ex-br  27863  rge0scvg  30593  repr0  31291  hgt750lemg  31334  mrsub0  32012  elmrsubrn  32016  topjoin  32948  pclfinN  36038  aomclem1  38565  dfac21  38577  clsk1indlem1  39281  fourierdlem102  41334  fourierdlem114  41346  lincval0  43201  lcoel0  43214