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

Theorem 3eltr3d 2522
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 2510 . 2  |-  ( ph  ->  A  e.  D )
51, 4eqeltrrd 2509 1  |-  ( ph  ->  C  e.  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-cleq 2412  df-clel 2415
This theorem is referenced by:  axcc2lem  8855  axcclem  8876  icoshftf1o  11742  lincmb01cmp  11762  fzosubel  11959  psgnunilem1  17086  efgcpbllemb  17346  lspprabs  18259  cnmpt2res  20629  xpstopnlem1  20761  tususp  21224  tustps  21225  ressxms  21477  ressms  21478  tmsxpsval  21490  limcco  22755  dvcnp2  22781  dvcnvlem  22835  taylthlem2  23233  jensen  23818  f1otrg  24788  txomap  28541  probmeasb  29130  cvmlift2lem9  29863  prdsbnd2  31875  iocopn  37254  icoopn  37259  reclimc  37354  cncfiooicclem1  37391  itgiccshift  37474  dirkercncflem4  37585  fourierdlem32  37618  fourierdlem33  37619  fourierdlem60  37646  fourierdlem61  37647  fourierdlem76  37662  fourierdlem81  37667  fourierdlem90  37676  fourierdlem111  37697
  Copyright terms: Public domain W3C validator