Theorem syl6eqelr 2697

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  wemoiso2  7045  releldm2  7109  mapprc  7748  ixpprc  7815  bren  7850  brdomg  7851  ctex  7856  domssex  8006  mapen  8009  ssenen  8019  fodomfib  8125  fi0  8209  dffi3  8220  brwdom  8355  brwdomn0  8357  unxpwdom2  8376  ixpiunwdom  8379  tcmin  8500  rankonid  8575  rankr1id  8608  cardf2  8652  cardid2  8662  carduni  8690  fseqen  8733  acndom  8757  acndom2  8760  alephnbtwn  8777  cardcf  8957  cfeq0  8961  cflim2  8968  coftr  8978  infpssr  9013  hsmexlem5  9135  axdc3lem4  9158  fodomb  9229  ondomon  9264  gruina  9519  ioof  12142  hashbc  13094  hashfacen  13095  trclun  13603  zsum  14296  fsum  14298  fsumcom2OLD  14348  fprod  14510  fprodcom2OLD  14554  xpsfrnel2  16048  eqgen  17470  symgbas  17623  symgfisg  17711  dvdsr  18469  asplss  19150  aspsubrg  19152  psrval  19183  clsf  20662  restco  20778  subbascn  20868  is2ndc  21059  ptbasin2  21191  ptbas  21192  indishmph  21411  ufldom  21576  cnextfres1  21682  ussid  21874  icopnfcld  22381  cnrehmeo  22560  csscld  22856  clsocv  22857  itg2gt0  23333  dvmptadd  23529  dvmptmul  23530  dvmptco  23541  logcn  24193  selberglem1  25034  wlkcompim  26054  wlkelwrd  26058  clwlkcompim  26292  hmopidmchi  28394  sigagensiga  29531  dya2iocbrsiga  29664  dya2icobrsiga  29665  fnessref  31522  unirep  32677  indexdom  32699  dicfnN  35490  pwslnmlem0  36679  mendval  36772  icof  38406  dvsubf  38802  fperdvper  38808  dvdivf  38812  itgsinexplem1  38845  stirlinglem7  38973  fourierdlem73  39072  fouriersw  39124  ovolval4lem1  39539