Theorem eqeltrrid 2317

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  dmrnssfld  4987  cnvexg  5266  opabbrex  6048  offval  6226  resfunexgALT  6253  abrexexg  6263  abrexex2g  6265  opabex3d  6266  oprssdmm  6317  unfidisj  7084  residfi  7107  ssfii  7141  djuexb  7211  nqprlu  7734  iccshftr  10190  iccshftl  10192  iccdil  10194  icccntr  10196  mertenslem2  12047  exprmfct  12660  infpnlem1  12882  4sqlem13m  12926  ennnfonelemg  12974  prdsval  13306  prdsbaslemss  13307  grpidvalg  13406  igsumvalx  13422  grppropstrg  13552  releqgg  13757  eqgex  13758  0opn  14680  difopn  14782  tgrest  14843  txbasex  14931  txdis1cn  14952  cnmptid  14955  cnmptc  14956  cnmpt1st  14962  cnmpt2nd  14963  cnmpt2c  14964  hmeoima  14984  hmeocld  14986  fsumcncntop  15241  expcn  15243  plycoeid3  15431