Theorem syl6eleqr 2176

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

Syntax hints:   → wi 4   = wceq 1285   ∈ wcel 1434

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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-clel 2079

This theorem is referenced by:  brelrng  4624  elabrex  5477  fliftel1  5513  ovidig  5697  unielxp  5879  2oconcl  6135  ecopqsi  6277  eroprf  6315  djulclr  6648  djurclr  6649  djulcl  6650  djurcl  6651  isnumi  6713  addclnq  6837  mulclnq  6838  recexnq  6852  ltexnqq  6870  prarloclemarch  6880  prarloclemarch2  6881  nnnq  6884  nqnq0  6903  addclnq0  6913  mulclnq0  6914  nqpnq0nq  6915  prarloclemlt  6955  prarloclemlo  6956  prarloclemcalc  6964  nqprm  7004  cauappcvgprlem2  7122  caucvgprlem2  7142  addclsr  7202  mulclsr  7203  prsrcl  7232  pitonnlem2  7287  pitore  7290  recnnre  7291  axaddcl  7304  axmulcl  7306  axcaucvglemcl  7333  axcaucvglemval  7335  axcaucvglemcau  7336  axcaucvglemres  7337  uztrn2  8931  eluz2nn  8952  peano2uzs  8967  rebtwn2z  9555  iseqfcl  9754  iseqfclt  9755  iser0  9787  bcm1k  10003  bcp1nk  10005  bcpasc  10009  hashennn  10023  hashcl  10024  climconst  10503  climshft2  10519  clim2iser  10549  clim2iser2  10550  iiserex  10551  serif0  10563  dvdsflip  10632  fzo0dvdseq  10638  gcdsupcl  10730  ialgr0  10806  prmind2  10882  crth  10980  djulclALT  11044  djurclALT  11045