Theorem syl5eleqr 2708

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

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

Assertion

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

Proof of Theorem syl5eleqr

Step	Hyp	Ref	Expression
1		syl5eleqr.1	. 2 |- A e. B
2		syl5eleqr.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2628	. 2 |- ( ph -> B = C )
4	1, 3	syl5eleq 2707	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  rabsnt  4266  onnev  5848  opabiota  6261  canth  6608  onnseq  7441  tfrlem16  7489  oen0  7666  nnawordex  7717  inf0  8518  cantnflt  8569  cnfcom2  8599  cnfcom3lem  8600  cnfcom3  8601  r1ordg  8641  r1val1  8649  rankr1id  8725  acacni  8962  dfacacn  8963  dfac13  8964  cda1dif  8998  ttukeylem5  9335  ttukeylem6  9336  gch2  9497  gch3  9498  gchac  9503  gchina  9521  swrds1  13451  wrdl3s3  13705  sadcp1  15177  lcmfunsnlem2  15353  xpsfrnel2  16225  idfucl  16541  gsumval2  17280  gsumz  17374  frmdmnd  17396  frmd0  17397  efginvrel2  18140  efgcpbl2  18170  pgpfaclem1  18480  lbsexg  19164  zringndrg  19838  frlmlbs  20136  mat0dimscm  20275  mat0scmat  20344  m2detleiblem5  20431  m2detleiblem6  20432  m2detleiblem3  20435  m2detleiblem4  20436  d0mat2pmat  20543  chpmat0d  20639  dfac14  21421  acufl  21721  cnextfvval  21869  cnextcn  21871  minveclem3b  23199  minveclem4a  23201  ovollb2  23257  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliun2  23274  ioombl1lem4  23329  uniioombllem1  23349  uniioombllem2  23351  uniioombllem6  23356  itg2monolem1  23517  itg2mono  23520  itg2cnlem1  23528  xrlimcnp  24695  efrlim  24696  eengbas  25861  ebtwntg  25862  ecgrtg  25863  elntg  25864  wlkl1loop  26534  wwlks2onv  26847  elwwlks2ons3  26848  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  ex-br  27288  rge0scvg  29995  repr0  30689  hgt750lemg  30732  mrsub0  31413  elmrsubrn  31417  topjoin  32360  pclfinN  35186  aomclem1  37624  dfac21  37636  clsk1indlem1  38343  fourierdlem102  40425  fourierdlem114  40437  lincval0  42204  lcoel0  42217