Theorem eqeltrrid 2319

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 2235	. 2 |- A = B
3		eqeltrrid.2	. 2 |- ( ph -> B e. C )
4	2, 3	eqeltrid 2318	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  dmrnssfld  4995  cnvexg  5274  opabbrex  6065  offval  6243  resfunexgALT  6270  abrexexg  6280  abrexex2g  6282  opabex3d  6283  oprssdmm  6334  unfidisj  7114  residfi  7139  ssfii  7173  djuexb  7243  nqprlu  7767  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  mertenslem2  12115  exprmfct  12728  infpnlem1  12950  4sqlem13m  12994  ennnfonelemg  13042  prdsval  13374  prdsbaslemss  13375  grpidvalg  13474  igsumvalx  13490  grppropstrg  13620  releqgg  13825  eqgex  13826  0opn  14749  difopn  14851  tgrest  14912  txbasex  15000  txdis1cn  15021  cnmptid  15024  cnmptc  15025  cnmpt1st  15031  cnmpt2nd  15032  cnmpt2c  15033  hmeoima  15053  hmeocld  15055  fsumcncntop  15310  expcn  15312  plycoeid3  15500