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

Theorem 3eltr4d 2557
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
StepHypRef Expression
1 3eltr4d.2 . 2  |-  ( ph  ->  C  =  A )
2 3eltr4d.1 . . 3  |-  ( ph  ->  A  e.  B )
3 3eltr4d.3 . . 3  |-  ( ph  ->  D  =  B )
42, 3eleqtrrd 2545 . 2  |-  ( ph  ->  A  e.  D )
51, 4eqeltrd 2542 1  |-  ( ph  ->  C  e.  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2446  df-clel 2449
This theorem is referenced by:  elimdelov  6279  ovmpt2dxf  6329  cantnflt  7994  cantnflem1  8011  cantnfltOLD  8024  cofsmo  8552  cfsmolem  8553  axcclem  8740  smobeth  8864  iccf1o  11549  revccat  12527  vdwlem8  14170  issubc3  14881  cofucl  14920  catccatid  15092  xpccatid  15120  mndpropd  15568  issubmnd  15571  pwspjmhm  15618  gsumccat  15641  mulgnndir  15771  imasgrp  15793  subg0cl  15811  subginvcl  15812  subgcl  15813  psgnunilem2  16123  efgsp1  16358  gsumzsubmcl  16526  gsumzsubmclOLD  16527  dpjghm  16687  pwsco1rhm  16952  pwsco2rhm  16953  isdrngd  16983  subrgmcl  17003  subrgunit  17009  issubdrg  17016  lmodprop2d  17133  psraddcl  17580  psrmulcllem  17584  psrvscacl  17590  qsssubdrg  18000  imacmp  19135  prdstps  19337  symgtgp  19807  tsmssub  19858  ustuqtop3  19953  utop2nei  19960  xpsxmetlem  20089  xpsmet  20092  imasf1oxms  20199  imasf1oms  20200  prdsmslem1  20237  prdsxmslem1  20238  prdsxmslem2  20239  tngngp2  20373  cnmpt2pc  20635  caublcls  20954  minveclem3a  21049  cvmliftlem7  27344  cvmliftlem10  27347  prdsbnd  28860  prdstotbnd  28861  prdsbnd2  28862  cnpwstotbnd  28864  repwsmet  28901  kelac1  29584  fnchoice  29919  stoweidlem26  29989  ovmpt2rdxf  30897  matgsum  31047  diblss  35173
  Copyright terms: Public domain W3C validator