Theorem 3eltr4d 2716

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

Step	Hyp	Ref	Expression
1		3eltr4d.2	. 2 |- ( ph -> C = A )
2		3eltr4d.1	. . 3 |- ( ph -> A e. B )
3		3eltr4d.3	. . 3 |- ( ph -> D = B )
4	2, 3	eleqtrrd 2704	. 2 |- ( ph -> A e. D )
5	1, 4	eqeltrd 2701	1 |- ( ph -> C e. D )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  elimdelov  6736  ovmpt2dxf  6786  cantnflt  8569  cantnflem1  8586  cofsmo  9091  cfsmolem  9092  axcclem  9279  smobeth  9408  iccf1o  12316  ccatw2s1p1  13413  revccat  13515  pwp1fsum  15114  vdwlem8  15692  issubc3  16509  cofucl  16548  catccatid  16752  xpccatid  16828  issstrmgm  17252  mndpropd  17316  issubmnd  17318  pwspjmhm  17368  gsumccat  17378  imasgrp  17531  mulgnndir  17569  mulgnndirOLD  17570  subg0cl  17602  subginvcl  17603  subgcl  17604  psgnunilem2  17915  efgsp1  18150  gsumzsubmcl  18318  dpjghm  18462  pwsco1rhm  18738  pwsco2rhm  18739  isdrngd  18772  subrgmcl  18792  subrgunit  18798  issubdrg  18805  lmodprop2d  18925  psraddcl  19383  psrmulcllem  19387  psrvscacl  19393  qsssubdrg  19805  matgsum  20243  mat1rhmcl  20287  dmatmulcl  20306  scmatghm  20339  imacmp  21200  prdstps  21432  symgtgp  21905  tsmssub  21952  ustuqtop3  22047  utop2nei  22054  xpsxmetlem  22184  xpsmet  22187  imasf1oxms  22294  imasf1oms  22295  prdsmslem1  22332  prdsxmslem1  22333  prdsxmslem2  22334  tngngp2  22456  cnmpt2pc  22727  caublcls  23107  minveclem3a  23198  efsubm  24297  wlkl1loop  26534  eucrct2eupth  27105  numclwwlkovf2exlem1  27211  cvmliftlem7  31273  cvmliftlem10  31276  prdsbnd  33592  prdstotbnd  33593  prdsbnd2  33594  cnpwstotbnd  33596  repwsmet  33633  diblss  36459  kelac1  37633  iunrelexpuztr  38011  fnchoice  39188  sumnnodd  39862  sublimc  39884  divlimc  39888  cncfshiftioo  40105  itgperiod  40197  stoweidlem26  40243  dirkercncflem2  40321  fourierdlem32  40356  fourierdlem33  40357  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem62  40385  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem81  40404  fourierdlem88  40411  fourierdlem89  40412  fourierdlem91  40414  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  fouriersw  40448  fouriercn  40449  uspgropssxp  41752  issubmgm2  41790  rnghmsubcsetclem1  41975  rnghmsubcsetclem2  41976  rngccatidALTV  41989  funcrngcsetc  41998  rhmsubcsetclem1  42021  rhmsubcsetclem2  42022  rhmsubcrngclem1  42027  rhmsubcrngclem2  42028  funcringcsetc  42035  ringccatidALTV  42052  srhmsubc  42076  rhmsubclem3  42088  rhmsubclem4  42089  srhmsubcALTV  42094  rhmsubcALTVlem3  42106  rhmsubcALTVlem4  42107  ovmpt2rdxf  42117