Theorem syl6eqelr 2890

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 2799	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		syl6eqelr.2	. 2 ⊢ 𝐵 ∈ 𝐶
4	2, 3	syl6eqel 2889	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1520   ∈ wcel 2079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-cleq 2786  df-clel 2861

This theorem is referenced by:  wemoiso2  7522  releldm2  7589  mapprc  8251  ixpprc  8321  bren  8356  brdomg  8357  domssex  8515  mapen  8518  ssenen  8528  fodomfib  8634  fi0  8720  dffi3  8731  brwdom  8867  brwdomn0  8869  unxpwdom2  8888  ixpiunwdom  8891  tcmin  9018  rankonid  9093  rankr1id  9126  cardf2  9207  cardid2  9217  carduni  9245  fseqen  9288  acndom  9312  acndom2  9315  alephnbtwn  9332  cardcf  9509  cfeq0  9513  cflim2  9520  coftr  9530  infpssr  9565  hsmexlem5  9687  axdc3lem4  9710  fodomb  9783  ondomon  9820  gruina  10075  ioof  12674  hashbc  13647  hashfacen  13648  trclun  14196  zsum  14896  fsum  14898  fprod  15116  eqgen  18074  symgbas  18227  symgfisg  18315  dvdsr  19074  asplss  19779  aspsubrg  19781  psrval  19818  clsf  21328  restco  21444  subbascn  21534  is2ndc  21726  ptbasin2  21858  ptbas  21859  indishmph  22078  ufldom  22242  cnextfres1  22348  ussid  22540  icopnfcld  23047  cnrehmeo  23228  csscld  23523  clsocv  23524  itg2gt0  24032  dvmptadd  24228  dvmptmul  24229  dvmptco  24240  logcn  24899  selberglem1  25791  hmopidmchi  29607  sigagensiga  30973  dya2iocbrsiga  31106  dya2icobrsiga  31107  logdivsqrle  31494  fnessref  33259  unirep  34466  indexdom  34487  dicfnN  37800  pwslnmlem0  39127  mendval  39219  icof  40975  dvsubf  41693  dvdivf  41702  itgsinexplem1  41734  stirlinglem7  41861  fourierdlem73  41960  fouriersw  42012  ovolval4lem1  42427