Theorem 3eltr4d 2291

Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)

Hypotheses

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

Assertion

Ref	Expression
3eltr4d	|- ( ph -> C e. D )

Proof of Theorem 3eltr4d

Step	Hyp	Ref	Expression
1		3eltr4d.2	. 2 |- ( ph -> C = A )
2		3eltr4d.1	. . 3 |- ( ph -> A e. B )
3		3eltr4d.3	. . 3 |- ( ph -> D = B )
4	2, 3	eleqtrrd 2287	. 2 |- ( ph -> A e. D )
5	1, 4	eqeltrd 2284	1 |- ( ph -> C e. D )

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

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 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  ovmpodxf  6094  nnaordi  6617  iccf1o  10161  nnmindc  12470  ennnfonelemrn  12905  ctiunctlemfo  12925  sgrppropd  13360  mndpropd  13387  issubmnd  13389  imasgrp  13562  mulgnndir  13602  subg0cl  13633  subginvcl  13634  subgcl  13635  rngcl  13821  rngpropd  13832  srgcl  13847  srgidcl  13853  ringidcl  13897  ringpropd  13915  dvdsrd  13971  dvrvald  14011  subrngmcl  14086  subrgmcl  14110  subrgunit  14116  lmodprop2d  14225  lidl0  14366  lidl1  14367  psraddcl  14557