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

Theorem 3eltr3d 2516
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 2512 . 2  |-  ( ph  ->  A  e.  D )
51, 4eqeltrrd 2511 1  |-  ( ph  ->  C  e.  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725
This theorem is referenced by:  axcc2lem  8316  axcclem  8337  icoshftf1o  11020  lincmb01cmp  11038  fzosubel  11177  efgcpbllemb  15387  lspprabs  16167  cnmpt2res  17709  xpstopnlem1  17841  tususp  18302  tustps  18303  ressxms  18555  ressms  18556  tmsxpsval  18568  limcco  19780  dvcnp2  19806  dvcnvlem  19860  taylthlem2  20290  jensen  20827  probmeasb  24688  cvmlift2lem9  24998  prdsbnd2  26504  psgnunilem1  27393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator