Theorem eqeltrrid 2265

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  dmrnssfld  4892  cnvexg  5168  opabbrex  5922  offval  6093  resfunexgALT  6112  abrexexg  6122  abrexex2g  6124  opabex3d  6125  oprssdmm  6175  unfidisj  6924  ssfii  6976  djuexb  7046  nqprlu  7549  iccshftr  9997  iccshftl  9999  iccdil  10001  icccntr  10003  mertenslem2  11547  exprmfct  12141  infpnlem1  12360  ennnfonelemg  12407  grpidvalg  12798  grppropstrg  12901  releqgg  13086  0opn  13646  difopn  13748  tgrest  13809  txbasex  13897  txdis1cn  13918  cnmptid  13921  cnmptc  13922  cnmpt1st  13928  cnmpt2nd  13929  cnmpt2c  13930  hmeoima  13950  hmeocld  13952  fsumcncntop  14196