Theorem eqeltrrid 2275

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

Syntax hints:   -> wi 4   = wceq 1363   e. wcel 2158

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183

This theorem is referenced by:  dmrnssfld  4902  cnvexg  5178  opabbrex  5932  offval  6104  resfunexgALT  6123  abrexexg  6133  abrexex2g  6135  opabex3d  6136  oprssdmm  6186  unfidisj  6935  ssfii  6987  djuexb  7057  nqprlu  7560  iccshftr  10008  iccshftl  10010  iccdil  10012  icccntr  10014  mertenslem2  11558  exprmfct  12152  infpnlem1  12371  ennnfonelemg  12418  grpidvalg  12811  grppropstrg  12925  releqgg  13120  eqgex  13121  0opn  13859  difopn  13961  tgrest  14022  txbasex  14110  txdis1cn  14131  cnmptid  14134  cnmptc  14135  cnmpt1st  14141  cnmpt2nd  14142  cnmpt2c  14143  hmeoima  14163  hmeocld  14165  fsumcncntop  14409