Theorem syl6eleq 1981

Description: A membership and equality inference.

Hypotheses

Ref	Expression
syl6eleq.1	|- (ph -> A e. B)
syl6eleq.2	|- B = C

Assertion

Ref	Expression
syl6eleq	|- (ph -> A e. C)

Proof of Theorem syl6eleq

Step	Hyp	Ref	Expression
1		syl6eleq.1	. 2 |- (ph -> A e. B)
2		syl6eleq.2	. . 3 |- B = C
3	2	a1i 8	. 2 |- (ph -> B = C)
4	1, 3	eleqtrd 1973	1 |- (ph -> A e. C)

Syntax hints:   -> wi 3   = wceq 1298   e. wcel 1300

This theorem is referenced by:  syl6eleqr 1982  prid2g 3105  ndmfvrcl 4703  tz7.48-1 5165  r1rankid 5805  rankelun 5818  rankelpr 5819  rankelop 5820  alephgeom 6030  icoshftf1oii 7578  eluz2 7590  binomlem1 8326  binomlem4 8329  binomlem5 8330  fsum0diaglem2 8519  fsum0diag3 8522  efaddlem6 8605  cnpco 9046  ghgrpilem1 9441  ghgrpilem3 9443  ghgrpilem4 9444  tx1cn 10223  tx2cn 10224  pjoc1i 10897  shmodsi 10995  5oalem1 11234  mayete3i 11308  mayete3OLDi 11309  adj1 11494  nmcopexlem4 11591  nmcfnexlem4 11620  bra11 11679  bnj1433 13128  bnj1244 13461  bnj1245 13463  bnj1450 13541  bnj1501 13570  suprzcl 13658  eucalg 13755  mulgcdlem2 13757  trclss 13935  bdayelon 14017  inposet 14620  seqzp2 14716  fictblem 15370  mettrifi2 15848  icccmp 16027  stbel 16729  osumcllem7 17370  pexmidlem4 17381

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-cleq 1877  df-clel 1880

Copyright terms: Public domain