Theorem eqeltrrid 2245

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

Syntax hints:   -> wi 4   = wceq 1335   e. wcel 2128

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153

This theorem is referenced by:  dmrnssfld  4846  cnvexg  5120  opabbrex  5859  offval  6033  resfunexgALT  6052  abrexexg  6060  abrexex2g  6062  opabex3d  6063  oprssdmm  6113  unfidisj  6859  ssfii  6911  djuexb  6978  nqprlu  7450  iccshftr  9880  iccshftl  9882  iccdil  9884  icccntr  9886  mertenslem2  11415  exprmfct  11994  ennnfonelemg  12104  0opn  12364  difopn  12468  tgrest  12529  txbasex  12617  txdis1cn  12638  cnmptid  12641  cnmptc  12642  cnmpt1st  12648  cnmpt2nd  12649  cnmpt2c  12650  hmeoima  12670  hmeocld  12672  fsumcncntop  12916