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

Theorem 3eltr4d 2493
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 2489 . 2  |-  ( ph  ->  A  e.  D )
51, 4eqeltrd 2486 1  |-  ( ph  ->  C  e.  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721
This theorem is referenced by:  elimdelov  6120  ovmpt2dxf  6166  cantnflt  7591  cofsmo  8113  cfsmolem  8114  axcclem  8301  smobeth  8425  iccf1o  11003  revccat  11761  vdwlem8  13319  issubc3  14009  cofucl  14048  catccatid  14220  xpccatid  14248  mndpropd  14684  issubmnd  14687  pwspjmhm  14730  gsumccat  14750  mulgnndir  14875  imasgrp  14897  subg0cl  14915  subginvcl  14916  subgcl  14917  efgsp1  15332  gsumzsubmcl  15486  dpjghm  15584  pwsco1rhm  15796  pwsco2rhm  15797  isdrngd  15823  subrgmcl  15843  subrgunit  15849  issubdrg  15856  lmodprop2d  15969  psraddcl  16410  psrmulcllem  16414  psrvscacl  16420  qsssubdrg  16721  imacmp  17422  prdstps  17622  symgtgp  18092  tsmssub  18139  ustuqtop3  18234  utop2nei  18241  xpsxmetlem  18370  xpsmet  18373  imasf1oxms  18480  imasf1oms  18481  prdsmslem1  18518  prdsxmslem1  18519  prdsxmslem2  18520  tngngp2  18654  cnmpt2pc  18914  caublcls  19222  minveclem3a  19289  cvmliftlem7  24939  cvmliftlem10  24942  prdsbnd  26400  prdstotbnd  26401  prdsbnd2  26402  cnpwstotbnd  26404  repwsmet  26441  kelac1  27037  psgnunilem2  27294  fnchoice  27575  stoweidlem26  27650  diblss  31665
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 1662  ax-8 1683  ax-11 1757  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2405  df-clel 2408
  Copyright terms: Public domain W3C validator