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

Theorem 3eltr4d 2518
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 2514 . 2  |-  ( ph  ->  A  e.  D )
51, 4eqeltrd 2511 1  |-  ( ph  ->  C  e.  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726
This theorem is referenced by:  elimdelov  6154  ovmpt2dxf  6200  cantnflt  7628  cofsmo  8150  cfsmolem  8151  axcclem  8338  smobeth  8462  iccf1o  11040  revccat  11799  vdwlem8  13357  issubc3  14047  cofucl  14086  catccatid  14258  xpccatid  14286  mndpropd  14722  issubmnd  14725  pwspjmhm  14768  gsumccat  14788  mulgnndir  14913  imasgrp  14935  subg0cl  14953  subginvcl  14954  subgcl  14955  efgsp1  15370  gsumzsubmcl  15524  dpjghm  15622  pwsco1rhm  15834  pwsco2rhm  15835  isdrngd  15861  subrgmcl  15881  subrgunit  15887  issubdrg  15894  lmodprop2d  16007  psraddcl  16448  psrmulcllem  16452  psrvscacl  16458  qsssubdrg  16759  imacmp  17461  prdstps  17662  symgtgp  18132  tsmssub  18179  ustuqtop3  18274  utop2nei  18281  xpsxmetlem  18410  xpsmet  18413  imasf1oxms  18520  imasf1oms  18521  prdsmslem1  18558  prdsxmslem1  18559  prdsxmslem2  18560  tngngp2  18694  cnmpt2pc  18954  caublcls  19262  minveclem3a  19329  cvmliftlem7  24979  cvmliftlem10  24982  prdsbnd  26503  prdstotbnd  26504  prdsbnd2  26505  cnpwstotbnd  26507  repwsmet  26544  kelac1  27139  psgnunilem2  27396  fnchoice  27677  stoweidlem26  27752  diblss  31969
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2430  df-clel 2433
  Copyright terms: Public domain W3C validator