Theorem syl6eqelr 2710

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

Hypotheses

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

Assertion

Ref	Expression
syl6eqelr	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl6eqelr

Step	Hyp	Ref	Expression
1		syl6eqelr.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2628	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		syl6eqelr.2	. 2 ⊢ 𝐵 ∈ 𝐶
4	2, 3	syl6eqel 2709	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  wemoiso2  7154  releldm2  7218  mapprc  7861  ixpprc  7929  bren  7964  brdomg  7965  ctex  7970  domssex  8121  mapen  8124  ssenen  8134  fodomfib  8240  fi0  8326  dffi3  8337  brwdom  8472  brwdomn0  8474  unxpwdom2  8493  ixpiunwdom  8496  tcmin  8617  rankonid  8692  rankr1id  8725  cardf2  8769  cardid2  8779  carduni  8807  fseqen  8850  acndom  8874  acndom2  8877  alephnbtwn  8894  cardcf  9074  cfeq0  9078  cflim2  9085  coftr  9095  infpssr  9130  hsmexlem5  9252  axdc3lem4  9275  fodomb  9348  ondomon  9385  gruina  9640  ioof  12271  hashbc  13237  hashfacen  13238  trclun  13755  zsum  14449  fsum  14451  fsumcom2OLD  14506  fprod  14671  fprodcom2OLD  14715  xpsfrnel2  16225  eqgen  17647  symgbas  17800  symgfisg  17888  dvdsr  18646  asplss  19329  aspsubrg  19331  psrval  19362  clsf  20852  restco  20968  subbascn  21058  is2ndc  21249  ptbasin2  21381  ptbas  21382  indishmph  21601  ufldom  21766  cnextfres1  21872  ussid  22064  icopnfcld  22571  cnrehmeo  22752  csscld  23048  clsocv  23049  itg2gt0  23527  dvmptadd  23723  dvmptmul  23724  dvmptco  23735  logcn  24393  selberglem1  25234  hmopidmchi  29010  sigagensiga  30204  dya2iocbrsiga  30337  dya2icobrsiga  30338  logdivsqrle  30728  fnessref  32352  unirep  33507  indexdom  33529  dicfnN  36472  pwslnmlem0  37661  mendval  37753  icof  39411  dvsubf  40128  dvdivf  40137  itgsinexplem1  40169  stirlinglem7  40297  fourierdlem73  40396  fouriersw  40448  ovolval4lem1  40863