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

Theorem 3eltr4d 2546
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 2534 . 2  |-  ( ph  ->  A  e.  D )
51, 4eqeltrd 2531 1  |-  ( ph  ->  C  e.  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-cleq 2435  df-clel 2438
This theorem is referenced by:  elimdelov  6363  ovmpt2dxf  6413  cantnflt  8094  cantnflem1  8111  cantnfltOLD  8124  cofsmo  8652  cfsmolem  8653  axcclem  8840  smobeth  8964  iccf1o  11675  revccat  12722  vdwlem8  14488  issubc3  15197  cofucl  15236  catccatid  15408  xpccatid  15436  mndpropd  15925  issubmnd  15927  pwspjmhm  15978  gsumccat  15988  mulgnndir  16143  imasgrp  16165  subg0cl  16188  subginvcl  16189  subgcl  16190  psgnunilem2  16499  efgsp1  16734  gsumzsubmcl  16907  gsumzsubmclOLD  16908  dpjghm  17091  pwsco1rhm  17366  pwsco2rhm  17367  isdrngd  17400  subrgmcl  17420  subrgunit  17426  issubdrg  17433  lmodprop2d  17551  psraddcl  18015  psrmulcllem  18019  psrvscacl  18025  qsssubdrg  18456  matgsum  18917  mat1rhmcl  18961  dmatmulcl  18980  scmatghm  19013  imacmp  19875  prdstps  20108  symgtgp  20578  tsmssub  20629  ustuqtop3  20724  utop2nei  20731  xpsxmetlem  20860  xpsmet  20863  imasf1oxms  20970  imasf1oms  20971  prdsmslem1  21008  prdsxmslem1  21009  prdsxmslem2  21010  tngngp2  21144  cnmpt2pc  21406  caublcls  21725  minveclem3a  21820  efsubm  22916  cvmliftlem7  28714  cvmliftlem10  28717  prdsbnd  30265  prdstotbnd  30266  prdsbnd2  30267  cnpwstotbnd  30269  repwsmet  30306  kelac1  30985  fnchoice  31358  sumnnodd  31590  sublimc  31612  divlimc  31616  cncfshiftioo  31649  itgperiod  31734  stoweidlem26  31762  dirkercncflem2  31840  fourierdlem32  31875  fourierdlem33  31876  fourierdlem46  31889  fourierdlem48  31891  fourierdlem49  31892  fourierdlem62  31905  fourierdlem74  31917  fourierdlem75  31918  fourierdlem76  31919  fourierdlem81  31924  fourierdlem88  31931  fourierdlem89  31932  fourierdlem91  31934  fourierdlem93  31936  fourierdlem103  31946  fourierdlem104  31947  fouriersw  31968  fouriercn  31969  issubmgm2  32432  rnghmsubcsetclem1  32658  rnghmsubcsetclem2  32659  rngccatidOLD  32672  funcrngcsetc  32681  rhmsubcsetclem1  32701  rhmsubcsetclem2  32702  rhmsubcrngclem1  32707  rhmsubcrngclem2  32708  funcringcsetc  32715  ringccatidOLD  32732  srhmsubc  32752  rhmsubclem3  32764  rhmsubclem4  32765  srhmsubcOLD  32771  rhmsubcOLDlem3  32783  rhmsubcOLDlem4  32784  ovmpt2rdxf  32796  diblss  36772
  Copyright terms: Public domain W3C validator