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

Theorem 3eltr4d 2570
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 2558 . 2  |-  ( ph  ->  A  e.  D )
51, 4eqeltrd 2555 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:  elimdelov  6361  ovmpt2dxf  6411  cantnflt  8090  cantnflem1  8107  cantnfltOLD  8120  cofsmo  8648  cfsmolem  8649  axcclem  8836  smobeth  8960  iccf1o  11663  revccat  12702  vdwlem8  14364  issubc3  15075  cofucl  15114  catccatid  15286  xpccatid  15314  mndpropd  15763  issubmnd  15766  pwspjmhm  15815  gsumccat  15838  mulgnndir  15971  imasgrp  15993  subg0cl  16011  subginvcl  16012  subgcl  16013  psgnunilem2  16323  efgsp1  16558  gsumzsubmcl  16728  gsumzsubmclOLD  16729  dpjghm  16911  pwsco1rhm  17182  pwsco2rhm  17183  isdrngd  17216  subrgmcl  17236  subrgunit  17242  issubdrg  17249  lmodprop2d  17367  psraddcl  17823  psrmulcllem  17827  psrvscacl  17833  qsssubdrg  18261  matgsum  18722  mat1rhmcl  18766  dmatmulcl  18785  scmatghm  18818  imacmp  19679  prdstps  19881  symgtgp  20351  tsmssub  20402  ustuqtop3  20497  utop2nei  20504  xpsxmetlem  20633  xpsmet  20636  imasf1oxms  20743  imasf1oms  20744  prdsmslem1  20781  prdsxmslem1  20782  prdsxmslem2  20783  tngngp2  20917  cnmpt2pc  21179  caublcls  21498  minveclem3a  21593  cvmliftlem7  28392  cvmliftlem10  28395  prdsbnd  29908  prdstotbnd  29909  prdsbnd2  29910  cnpwstotbnd  29912  repwsmet  29949  kelac1  30629  fnchoice  30998  stoweidlem26  31342  ovmpt2rdxf  32012  diblss  35976
  Copyright terms: Public domain W3C validator