Theorem eqeltrid 2264

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

Hypotheses

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

Assertion

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

Proof of Theorem eqeltrid

Step	Hyp	Ref	Expression
1		eqeltrid.1	. . 3 |- A = B
2	1	a1i 9	. 2 |- ( ph -> A = B )
3		eqeltrid.2	. 2 |- ( ph -> B e. C )
4	2, 3	eqeltrd 2254	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eqeltrrid  2265  csbexga  4131  otexg  4230  tpexg  4444  dmresexg  4930  f1oabexg  5473  funfvex  5532  riotaexg  5834  riotaprop  5853  fnovex  5907  ovexg  5908  fovcdm  6016  fnovrn  6021  cofunexg  6109  cofunex2g  6110  abrexex2g  6120  xpexgALT  6133  mpofvex  6203  tfrex  6368  frec0g  6397  freccllem  6402  ecexg  6538  qsexg  6590  pmex  6652  elixpsn  6734  diffifi  6893  unfidisj  6920  prfidisj  6925  tpfidisj  6926  ssfirab  6932  ssfidc  6933  fnfi  6935  funrnfi  6940  iunfidisj  6944  infclti  7021  supex2g  7031  infex2g  7032  djuex  7041  ctssdccl  7109  addvalex  7842  negcl  8156  intqfrac2  10318  intfracq  10319  frec2uzzd  10399  frecuzrdgrrn  10407  iseqf1olemqpcl  10495  seq3f1olemqsum  10499  bcval5  10742  xrmaxiflemval  11257  climmpt  11307  reccn2ap  11320  zsumdc  11391  fsumzcl2  11412  fsump1i  11440  fsumabs  11472  hash2iun1dif1  11487  mertenslemi1  11542  fprodcllemf  11620  algrf  12044  algcvg  12047  algcvga  12050  algfx  12051  eucalgcvga  12057  eucalg  12058  crth  12223  phimullem  12224  eulerthlemth  12231  prmdiv  12234  pythagtriplem11  12273  pythagtriplem13  12275  pcprecl  12288  infpnlem1  12356  infpnlem2  12357  4sqlem5  12379  mul4sqlem  12390  ennnfonelemj0  12401  ennnfonelemom  12408  ressval3d  12530  1strbas  12575  2strbasg  12577  2stropg  12578  restid  12698  topnvalg  12699  topnidg  12700  imasival  12726  imasmulr  12729  imasaddfn  12737  imasaddval  12738  imasaddf  12739  imasmulfn  12740  imasmulval  12741  imasmulf  12742  qusval  12743  qusaddval  12753  qusaddf  12754  qusmulval  12755  qusmulf  12756  xpsval  12770  plusffvalg  12780  plusfvalg  12781  grpidvalg  12791  issubmnd  12842  ress0g  12843  ismhm  12852  0mhm  12872  grpinvfvalg  12914  grpinvval  12915  grpinvfng  12916  grpsubfvalg  12917  grpsubval  12918  grpressid  12930  grplactfval  12970  mulgfvalg  12984  mulgval  12985  mulgfng  12986  mulgnnp1  12990  mulgnndir  13010  issubg  13031  subggrp  13035  issubg2m  13047  eqgfval  13079  eqgen  13084  mgpvalg  13131  mgpplusgg  13132  mgptopng  13137  mgpress  13139  issrg  13146  ringidss  13210  ring1  13234  ringressid  13236  opprvalg  13239  opprmulfvalg  13240  rdivmuldivd  13311  issubrg  13340  subrgring  13343  islmod  13379  scaffvalg  13394  scafvalg  13395  topopn  13478  topcld  13579  uncld  13583  iuncld  13585  unicld  13586  tgrest  13639  restin  13646  cnco  13691  cnrest  13705  cnptoprest2  13710  lmss  13716  txbasval  13737  txcn  13745  cnmpt12f  13756  hmeoco  13786  idhmeo  13787  blres  13904  metrest  13976  qtopbasss  13991  tgqioo  14017  divcnap  14025  fsumcncntop  14026  cncfmet  14049  cdivcncfap  14057  cnrehmeocntop  14063  cnplimcim  14106  limccnpcntop  14114  limccnp2lem  14115  limccnp2cntop  14116  dvfvalap  14120  lgseisenlem1  14420  lgseisenlem2  14421  2sqlem8  14440  bj-snexg  14634  trilpolemcl  14755