Theorem syl6eleqr 2172

Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)

Hypotheses

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

Assertion

Ref	Expression
syl6eleqr	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl6eleqr

Step	Hyp	Ref	Expression
1		syl6eleqr.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		syl6eleqr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2085	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6eleq 2171	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1284   ∈ wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  brelrng  4583  elabrex  5418  fliftel1  5454  ovidig  5638  unielxp  5820  2oconcl  6045  ecopqsi  6184  eroprf  6222  isnumi  6451  addclnq  6565  mulclnq  6566  recexnq  6580  ltexnqq  6598  prarloclemarch  6608  prarloclemarch2  6609  nnnq  6612  nqnq0  6631  addclnq0  6641  mulclnq0  6642  nqpnq0nq  6643  prarloclemlt  6683  prarloclemlo  6684  prarloclemcalc  6692  nqprm  6732  cauappcvgprlem2  6850  caucvgprlem2  6870  addclsr  6930  mulclsr  6931  prsrcl  6960  pitonnlem2  7015  pitore  7018  recnnre  7019  axaddcl  7032  axmulcl  7034  axcaucvglemcl  7061  axcaucvglemval  7063  axcaucvglemcau  7064  axcaucvglemres  7065  uztrn2  8636  eluz2nn  8657  peano2uzs  8672  rebtwn2z  9263  iser0  9471  bcm1k  9687  bcp1nk  9689  bcpasc  9693  climconst  10129  climshft2  10145  clim2iser  10175  clim2iser2  10176  iiserex  10177  serif0  10189  dvdsflip  10251  fzo0dvdseq  10257  gcdsupcl  10350  ialgr0  10426  prmind2  10502