Theorem syl6eleqr 2178

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

Syntax hints:   → wi 4   = wceq 1287   ∈ wcel 1436

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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081

This theorem is referenced by:  brelrng  4636  elabrex  5500  fliftel1  5536  ovidig  5721  unielxp  5903  2oconcl  6159  ecopqsi  6301  eroprf  6339  sbthlem2  6614  djulclr  6688  djurclr  6689  djulcl  6690  djurcl  6691  isnumi  6757  addclnq  6881  mulclnq  6882  recexnq  6896  ltexnqq  6914  prarloclemarch  6924  prarloclemarch2  6925  nnnq  6928  nqnq0  6947  addclnq0  6957  mulclnq0  6958  nqpnq0nq  6959  prarloclemlt  6999  prarloclemlo  7000  prarloclemcalc  7008  nqprm  7048  cauappcvgprlem2  7166  caucvgprlem2  7186  addclsr  7246  mulclsr  7247  prsrcl  7276  pitonnlem2  7331  pitore  7334  recnnre  7335  axaddcl  7348  axmulcl  7350  axcaucvglemcl  7377  axcaucvglemval  7379  axcaucvglemcau  7380  axcaucvglemres  7381  uztrn2  8971  eluz2nn  8992  peano2uzs  9007  rebtwn2z  9597  iseqfcl  9796  iseqfclt  9797  iser0  9851  bcm1k  10068  bcp1nk  10070  bcpasc  10074  hashennn  10088  hashcl  10089  climconst  10576  climshft2  10592  clim2iser  10622  clim2iser2  10623  iiserex  10624  serif0  10636  zisum  10668  dvdsflip  10758  fzo0dvdseq  10764  gcdsupcl  10856  ialgr0  10932  prmind2  11008  crth  11106  djulclALT  11170  djurclALT  11171