Theorem syl6eqelr 2739

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

Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647

This theorem is referenced by:  wemoiso2  7196  releldm2  7262  mapprc  7903  ixpprc  7971  bren  8006  brdomg  8007  ctex  8012  domssex  8162  mapen  8165  ssenen  8175  fodomfib  8281  fi0  8367  dffi3  8378  brwdom  8513  brwdomn0  8515  unxpwdom2  8534  ixpiunwdom  8537  tcmin  8655  rankonid  8730  rankr1id  8763  cardf2  8807  cardid2  8817  carduni  8845  fseqen  8888  acndom  8912  acndom2  8915  alephnbtwn  8932  cardcf  9112  cfeq0  9116  cflim2  9123  coftr  9133  infpssr  9168  hsmexlem5  9290  axdc3lem4  9313  fodomb  9386  ondomon  9423  gruina  9678  ioof  12309  hashbc  13275  hashfacen  13276  trclun  13799  zsum  14493  fsum  14495  fsumcom2OLD  14550  fprod  14715  fprodcom2OLD  14759  xpsfrnel2  16272  eqgen  17694  symgbas  17846  symgfisg  17934  dvdsr  18692  asplss  19377  aspsubrg  19379  psrval  19410  clsf  20900  restco  21016  subbascn  21106  is2ndc  21297  ptbasin2  21429  ptbas  21430  indishmph  21649  ufldom  21813  cnextfres1  21919  ussid  22111  icopnfcld  22618  cnrehmeo  22799  csscld  23094  clsocv  23095  itg2gt0  23572  dvmptadd  23768  dvmptmul  23769  dvmptco  23780  logcn  24438  selberglem1  25279  hmopidmchi  29138  sigagensiga  30332  dya2iocbrsiga  30465  dya2icobrsiga  30466  logdivsqrle  30856  fnessref  32477  unirep  33637  indexdom  33659  dicfnN  36789  pwslnmlem0  37978  mendval  38070  icof  39725  dvsubf  40446  dvdivf  40455  itgsinexplem1  40487  stirlinglem7  40615  fourierdlem73  40714  fouriersw  40766  ovolval4lem1  41184