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 1398   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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

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

This theorem is referenced by:  dmrnssfld  5001  cnvexg  5281  opabbrex  6075  offval  6252  resfunexgALT  6279  abrexexg  6289  abrexex2g  6291  opabex3d  6292  oprssdmm  6343  unfidisj  7157  residfi  7182  ssfii  7233  djuexb  7303  nqprlu  7827  iccshftr  10290  iccshftl  10292  iccdil  10294  icccntr  10296  mertenslem2  12177  exprmfct  12790  infpnlem1  13012  4sqlem13m  13056  ennnfonelemg  13104  prdsval  13436  prdsbaslemss  13437  grpidvalg  13536  igsumvalx  13552  grppropstrg  13682  releqgg  13887  eqgex  13888  0opn  14817  difopn  14919  tgrest  14980  txbasex  15068  txdis1cn  15089  cnmptid  15092  cnmptc  15093  cnmpt1st  15099  cnmpt2nd  15100  cnmpt2c  15101  hmeoima  15121  hmeocld  15123  fsumcncntop  15378  expcn  15380  plycoeid3  15568