Theorem syl6eqel 1556

Description: A membership and equality inference.

Hypotheses

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

Assertion

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

Proof of Theorem syl6eqel

Step	Hyp	Ref	Expression
1		syl6eqel.1	. 2 |- (ph -> A = B)
2		syl6eqel.2	. . 3 |- B e. C
3	2	a1i 8	. 2 |- (ph -> B e. C)
4	1, 3	eqeltrd 1548	1 |- (ph -> A e. C)

Syntax hints:   -> wi 3   = wceq 956   e. wcel 958

This theorem is referenced by:  syl6eqelr 1557  class2set 2734  moabex 2766  prex 2781  unisn2 2875  onun 3110  relsn 3254  zfrep6 3614  elimdeloprv 4001  ndmoprcl 4044  oesuc 4166  omcl 4171  oecl 4172  nnmcl 4230  nnecl 4231  xpsnen 4435  pw2en 4446  noinfep 4640  rankon 4671  alephon 4865  recclpq 5072  nn0addclt 6120  nn0mulcl 6122  znegclt 6163  elnn0nn 6171  zeot 6199  limsupclt 6530  expcllem 6575  faclbnd4lem3 6950  bccl2t 6971  bcclt 6972  serzcmp0 7055  bcxmas 7076  iserzcmp0 7143  eirrlem4 7392  eirrlem5 7393  acdc3lem 7486  acdc2lem1 7488  acdclem 7494  infpnlem2 7507  sn0top 7647  indistop 7648  iooretop 7659  0blo 8452  nmlno0lem 8453  resslogrn 8753  omlsilem 9244  pjoc1 9264  nonbool 9596  nmlnop0ALT 9920  unopbdt 9940  lnopcon 9963  lnfncon 9990  leoprf2t 10060  pjbdln 10076  pjcmmul1 10129  eloi 10659  aidm 10683  aidmold 10684

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain