Theorem syl6eleqr 2193

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

Syntax hints:   → wi 4   = wceq 1299   ∈ wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096

This theorem is referenced by:  brelrng  4708  elabrex  5591  fliftel1  5627  ovidig  5820  unielxp  6002  2oconcl  6266  ecopqsi  6414  eroprf  6452  sbthlem2  6774  djulclr  6849  djurclr  6850  djulcl  6851  djurcl  6852  caseinl  6891  caseinr  6892  isnumi  6949  addclnq  7084  mulclnq  7085  recexnq  7099  ltexnqq  7117  prarloclemarch  7127  prarloclemarch2  7128  nnnq  7131  nqnq0  7150  addclnq0  7160  mulclnq0  7161  nqpnq0nq  7162  prarloclemlt  7202  prarloclemlo  7203  prarloclemcalc  7211  nqprm  7251  cauappcvgprlem2  7369  caucvgprlem2  7389  addclsr  7449  mulclsr  7450  prsrcl  7479  pitonnlem2  7534  pitore  7537  recnnre  7538  axaddcl  7551  axmulcl  7553  axcaucvglemcl  7580  axcaucvglemval  7582  axcaucvglemcau  7583  axcaucvglemres  7584  uztrn2  9193  eluz2nn  9214  peano2uzs  9229  rebtwn2z  9873  seqf  10075  ser0  10128  bcm1k  10347  bcp1nk  10349  bcpasc  10353  hashennn  10367  hashcl  10368  climconst  10898  climshft2  10914  clim2ser  10945  clim2ser2  10946  iserex  10947  serf0  10960  zsumdc  10992  fsump1i  11041  iserabs  11083  isumshft  11098  isumsplit  11099  isum1p  11100  isumrpcl  11102  cvgratnnlemseq  11134  cvgratz  11140  cvgratgt0  11141  ef0lem  11164  dvdsflip  11344  fzo0dvdseq  11350  gcdsupcl  11442  ialgr0  11518  prmind2  11594  crth  11692  ennnfonelemkh  11717  ennnfonelemrn  11724  ennnfonelemdm  11725  strslfv2d  11783  1strbas  11840  2strbasg  11842  2stropg  11843  2strbas1g  11845  rngbaseg  11857  rngplusgg  11858  rngmulrg  11859  srngbased  11864  srngplusgd  11865  srngmulrd  11866  srnginvld  11867  lmodbased  11875  lmodplusgd  11876  lmodscad  11877  lmodvscad  11878  ipsbased  11883  ipsaddgd  11884  ipsmulrd  11885  ipsscad  11886  ipsvscad  11887  ipsipd  11888  topgrpbasd  11893  topgrpplusgd  11894  topgrptsetd  11895  lmconst  12166  lmss  12196  uptx  12224  cnmpt1res  12246  dvidlemap  12533  djulclALT  12589  djurclALT  12590  pwle2  12779  trilpolemeq1  12817