Theorem eqeltrrid 2326

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  dmrnssfld  5045  cnvexg  5325  opabbrex  6132  offval  6310  resfunexgALT  6337  abrexexg  6347  abrexex2g  6349  opabex3d  6350  oprssdmm  6405  unfidisj  7229  residfi  7254  ssfii  7308  djuexb  7385  nqprlu  7915  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  mertenslem2  12322  exprmfct  12936  infpnlem1  13161  4sqlem13m  13205  ballotfilemfrcn0  13325  ennnfonelemg  13346  grpidvalg  13746  gzsumvalx  13762  grppropstrg  13877  releqgg  14076  eqgex  14077  prdsval  14257  prdsbaslemss  14258  aprprop  14685  issubassa  15097  0opn  15198  difopn  15300  tgrest  15361  txbasex  15449  txdis1cn  15470  cnmptid  15473  cnmptc  15474  cnmpt1st  15480  cnmpt2nd  15481  cnmpt2c  15482  hmeoima  15502  hmeocld  15504  fsumcncntop  15759  expcn  15761  plycoeid3  15949