MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eltr3d Structured version   Unicode version

Theorem 3eltr3d 2569
Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
3eltr3d.1  |-  ( ph  ->  A  e.  B )
3eltr3d.2  |-  ( ph  ->  A  =  C )
3eltr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eltr3d  |-  ( ph  ->  C  e.  D )

Proof of Theorem 3eltr3d
StepHypRef Expression
1 3eltr3d.2 . 2  |-  ( ph  ->  A  =  C )
2 3eltr3d.1 . . 3  |-  ( ph  ->  A  e.  B )
3 3eltr3d.3 . . 3  |-  ( ph  ->  B  =  D )
42, 3eleqtrd 2557 . 2  |-  ( ph  ->  A  e.  D )
51, 4eqeltrrd 2556 1  |-  ( ph  ->  C  e.  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462
This theorem is referenced by:  axcc2lem  8817  axcclem  8838  icoshftf1o  11644  lincmb01cmp  11664  fzosubel  11844  psgnunilem1  16333  efgcpbllemb  16588  lspprabs  17553  cnmpt2res  20005  xpstopnlem1  20137  tususp  20602  tustps  20603  ressxms  20855  ressms  20856  tmsxpsval  20868  limcco  22124  dvcnp2  22150  dvcnvlem  22204  taylthlem2  22595  jensen  23143  probmeasb  28120  cvmlift2lem9  28507  prdsbnd2  30121
  Copyright terms: Public domain W3C validator