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

Theorem 3eltr4d 2519
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 2515 . 2  |-  ( ph  ->  A  e.  D )
51, 4eqeltrd 2512 1  |-  ( ph  ->  C  e.  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-clel 2434
This theorem is referenced by:  elimdelov  6162  ovmpt2dxf  6211  cantnflt  7872  cantnflem1  7889  cantnfltOLD  7902  cofsmo  8430  cfsmolem  8431  axcclem  8618  smobeth  8742  iccf1o  11421  revccat  12398  vdwlem8  14041  issubc3  14751  cofucl  14790  catccatid  14962  xpccatid  14990  mndpropd  15438  issubmnd  15441  pwspjmhm  15487  gsumccat  15510  mulgnndir  15640  imasgrp  15662  subg0cl  15680  subginvcl  15681  subgcl  15682  psgnunilem2  15992  efgsp1  16225  gsumzsubmcl  16393  gsumzsubmclOLD  16394  dpjghm  16550  pwsco1rhm  16808  pwsco2rhm  16809  isdrngd  16835  subrgmcl  16855  subrgunit  16861  issubdrg  16868  lmodprop2d  16985  psraddcl  17431  psrmulcllem  17435  psrvscacl  17441  qsssubdrg  17847  imacmp  18975  prdstps  19177  symgtgp  19647  tsmssub  19698  ustuqtop3  19793  utop2nei  19800  xpsxmetlem  19929  xpsmet  19932  imasf1oxms  20039  imasf1oms  20040  prdsmslem1  20077  prdsxmslem1  20078  prdsxmslem2  20079  tngngp2  20213  cnmpt2pc  20475  caublcls  20794  minveclem3a  20889  cvmliftlem7  27132  cvmliftlem10  27135  prdsbnd  28645  prdstotbnd  28646  prdsbnd2  28647  cnpwstotbnd  28649  repwsmet  28686  kelac1  29369  fnchoice  29704  stoweidlem26  29774  ovmpt2rdxf  30681  matgsum  30785  diblss  34655
  Copyright terms: Public domain W3C validator