Theorem eqeltrrid 2293

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  dmrnssfld  4942  cnvexg  5221  opabbrex  5991  offval  6168  resfunexgALT  6195  abrexexg  6205  abrexex2g  6207  opabex3d  6208  oprssdmm  6259  unfidisj  7021  residfi  7044  ssfii  7078  djuexb  7148  nqprlu  7662  iccshftr  10118  iccshftl  10120  iccdil  10122  icccntr  10124  mertenslem2  11880  exprmfct  12493  infpnlem1  12715  4sqlem13m  12759  ennnfonelemg  12807  prdsval  13138  prdsbaslemss  13139  grpidvalg  13238  igsumvalx  13254  grppropstrg  13384  releqgg  13589  eqgex  13590  0opn  14511  difopn  14613  tgrest  14674  txbasex  14762  txdis1cn  14783  cnmptid  14786  cnmptc  14787  cnmpt1st  14793  cnmpt2nd  14794  cnmpt2c  14795  hmeoima  14815  hmeocld  14817  fsumcncntop  15072  expcn  15074  plycoeid3  15262