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  6064  offval  6242  resfunexgALT  6269  abrexexg  6279  abrexex2g  6281  opabex3d  6282  oprssdmm  6333  unfidisj  7113  residfi  7138  ssfii  7172  djuexb  7242  nqprlu  7766  iccshftr  10228  iccshftl  10230  iccdil  10232  icccntr  10234  mertenslem2  12096  exprmfct  12709  infpnlem1  12931  4sqlem13m  12975  ennnfonelemg  13023  prdsval  13355  prdsbaslemss  13356  grpidvalg  13455  igsumvalx  13471  grppropstrg  13601  releqgg  13806  eqgex  13807  0opn  14729  difopn  14831  tgrest  14892  txbasex  14980  txdis1cn  15001  cnmptid  15004  cnmptc  15005  cnmpt1st  15011  cnmpt2nd  15012  cnmpt2c  15013  hmeoima  15033  hmeocld  15035  fsumcncntop  15290  expcn  15292  plycoeid3  15480