Theorem eqeltrrid 2294

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  dmrnssfld  4949  cnvexg  5228  opabbrex  6001  offval  6178  resfunexgALT  6205  abrexexg  6215  abrexex2g  6217  opabex3d  6218  oprssdmm  6269  unfidisj  7033  residfi  7056  ssfii  7090  djuexb  7160  nqprlu  7675  iccshftr  10131  iccshftl  10133  iccdil  10135  icccntr  10137  mertenslem2  11917  exprmfct  12530  infpnlem1  12752  4sqlem13m  12796  ennnfonelemg  12844  prdsval  13175  prdsbaslemss  13176  grpidvalg  13275  igsumvalx  13291  grppropstrg  13421  releqgg  13626  eqgex  13627  0opn  14548  difopn  14650  tgrest  14711  txbasex  14799  txdis1cn  14820  cnmptid  14823  cnmptc  14824  cnmpt1st  14830  cnmpt2nd  14831  cnmpt2c  14832  hmeoima  14852  hmeocld  14854  fsumcncntop  15109  expcn  15111  plycoeid3  15299