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

Theorem 3eltr4d 2468
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 2464 . 2  |-  ( ph  ->  A  e.  D )
51, 4eqeltrd 2461 1  |-  ( ph  ->  C  e.  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717
This theorem is referenced by:  elimdelov  6092  ovmpt2dxf  6138  cantnflt  7560  cofsmo  8082  cfsmolem  8083  axcclem  8270  smobeth  8394  iccf1o  10971  revccat  11725  vdwlem8  13283  issubc3  13973  cofucl  14012  catccatid  14184  xpccatid  14212  mndpropd  14648  issubmnd  14651  pwspjmhm  14694  gsumccat  14714  mulgnndir  14839  imasgrp  14861  subg0cl  14879  subginvcl  14880  subgcl  14881  efgsp1  15296  gsumzsubmcl  15450  dpjghm  15548  pwsco1rhm  15760  pwsco2rhm  15761  isdrngd  15787  subrgmcl  15807  subrgunit  15813  issubdrg  15820  lmodprop2d  15933  psraddcl  16374  psrmulcllem  16378  psrvscacl  16384  qsssubdrg  16681  imacmp  17382  prdstps  17582  symgtgp  18052  tsmssub  18099  ustuqtop3  18194  utop2nei  18201  xpsxmetlem  18317  xpsmet  18320  imasf1oxms  18409  imasf1oms  18410  prdsmslem1  18447  prdsxmslem1  18448  prdsxmslem2  18449  tngngp2  18564  cnmpt2pc  18824  caublcls  19132  minveclem3a  19195  cvmliftlem7  24757  cvmliftlem10  24760  prdsbnd  26193  prdstotbnd  26194  prdsbnd2  26195  cnpwstotbnd  26197  repwsmet  26234  kelac1  26830  psgnunilem2  27087  fnchoice  27368  stoweidlem26  27443  diblss  31285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2380  df-clel 2383
  Copyright terms: Public domain W3C validator