Theorem eqeltrrdi 2321

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eqeltrrdi.1	|- ( ph -> B = A )
eqeltrrdi.2	|- B e. C

Assertion

Ref	Expression
eqeltrrdi	|- ( ph -> A e. C )

Proof of Theorem eqeltrrdi

Step	Hyp	Ref	Expression
1		eqeltrrdi.1	. . 3 |- ( ph -> B = A )
2	1	eqcomd 2235	. 2 |- ( ph -> A = B )
3		eqeltrrdi.2	. 2 |- B e. C
4	2, 3	eqeltrdi 2320	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:  eusvnfb  4545  releldm2  6331  mapprc  6799  ixpprc  6866  ixpssmap2g  6874  ixpssmapg  6875  bren  6895  brdomg  6897  mapen  7007  ssenen  7012  fi0  7142  nnnninf2  7294  ioof  10167  hashfacen  11058  fsum3  11898  psrval  14630  cnrehmeocntop  15284