Theorem eqeltrrid 2227

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

Syntax hints:   -> wi 4   = wceq 1331   e. wcel 1480

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  dmrnssfld  4802  cnvexg  5076  opabbrex  5815  offval  5989  resfunexgALT  6008  abrexexg  6016  abrexex2g  6018  opabex3d  6019  oprssdmm  6069  unfidisj  6810  ssfii  6862  djuexb  6929  nqprlu  7358  iccshftr  9780  iccshftl  9782  iccdil  9784  icccntr  9786  mertenslem2  11308  exprmfct  11821  ennnfonelemg  11919  0opn  12176  difopn  12280  tgrest  12341  txbasex  12429  txdis1cn  12450  cnmptid  12453  cnmptc  12454  cnmpt1st  12460  cnmpt2nd  12461  cnmpt2c  12462  hmeoima  12482  hmeocld  12484  fsumcncntop  12728