Theorem eqeltrrid 2254

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

Hypotheses

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

Assertion

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

Proof of Theorem eqeltrrid

Step	Hyp	Ref	Expression
1		eqeltrrid.1	. . 3 |- B = A
2	1	eqcomi 2169	. 2 |- A = B
3		eqeltrrid.2	. 2 |- ( ph -> B e. C )
4	2, 3	eqeltrid 2253	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  dmrnssfld  4867  cnvexg  5141  opabbrex  5886  offval  6057  resfunexgALT  6076  abrexexg  6086  abrexex2g  6088  opabex3d  6089  oprssdmm  6139  unfidisj  6887  ssfii  6939  djuexb  7009  nqprlu  7488  iccshftr  9930  iccshftl  9932  iccdil  9934  icccntr  9936  mertenslem2  11477  exprmfct  12070  infpnlem1  12289  ennnfonelemg  12336  grpidvalg  12604  0opn  12644  difopn  12748  tgrest  12809  txbasex  12897  txdis1cn  12918  cnmptid  12921  cnmptc  12922  cnmpt1st  12928  cnmpt2nd  12929  cnmpt2c  12930  hmeoima  12950  hmeocld  12952  fsumcncntop  13196