Theorem syl6eqelr 2862

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

Syntax hints:   → wi 4   = wceq 1634   ∈ wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-ext 2754

This theorem depends on definitions:  df-bi 198  df-an 384  df-ex 1856  df-cleq 2767  df-clel 2770

This theorem is referenced by:  wemoiso2  7322  releldm2  7388  mapprc  8034  ixpprc  8104  bren  8139  brdomg  8140  ctex  8145  domssex  8298  mapen  8301  ssenen  8311  fodomfib  8417  fi0  8503  dffi3  8514  brwdom  8649  brwdomn0  8651  unxpwdom2  8670  ixpiunwdom  8673  tcmin  8802  rankonid  8877  rankr1id  8910  cardf2  8990  cardid2  9000  carduni  9028  fseqen  9071  acndom  9095  acndom2  9098  alephnbtwn  9115  cardcf  9297  cfeq0  9301  cflim2  9308  coftr  9318  infpssr  9353  hsmexlem5  9475  axdc3lem4  9498  fodomb  9571  ondomon  9608  gruina  9863  ioof  12496  hashbc  13461  hashfacen  13462  trclun  13985  zsum  14679  fsum  14681  fprod  14900  xpsfrnel2  16453  eqgen  17875  symgbas  18027  symgfisg  18115  dvdsr  18874  asplss  19564  aspsubrg  19566  psrval  19597  clsf  21093  restco  21209  subbascn  21299  is2ndc  21490  ptbasin2  21622  ptbas  21623  indishmph  21842  ufldom  22006  cnextfres1  22112  ussid  22304  icopnfcld  22811  cnrehmeo  22992  csscld  23287  clsocv  23288  itg2gt0  23768  dvmptadd  23964  dvmptmul  23965  dvmptco  23976  logcn  24635  selberglem1  25476  hmopidmchi  29367  sigagensiga  30561  dya2iocbrsiga  30694  dya2icobrsiga  30695  logdivsqrle  31085  fnessref  32706  unirep  33856  indexdom  33878  dicfnN  37008  pwslnmlem0  38202  mendval  38294  icof  39940  dvsubf  40652  dvdivf  40661  itgsinexplem1  40693  stirlinglem7  40820  fourierdlem73  40919  fouriersw  40971  ovolval4lem1  41389