Theorem 3eltr4d 2854

Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)

Hypotheses

Ref	Expression
3eltr4d.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
3eltr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eltr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eltr4d	⊢ (𝜑 → 𝐶 ∈ 𝐷)

Proof of Theorem 3eltr4d

Step	Hyp	Ref	Expression
1		3eltr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3eltr4d.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
3		3eltr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
4	2, 3	eleqtrrd 2842	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
5	1, 4	eqeltrd 2839	1 ⊢ (𝜑 → 𝐶 ∈ 𝐷)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816

This theorem is referenced by:  elimdelov  7362  ovmpodxf  7414  cantnflt  9418  cantnflem1  9435  cofsmo  10013  cfsmolem  10014  axcclem  10201  smobeth  10330  iccf1o  13216  ccatw2s1p1  14334  ccatw2s1p1OLD  14335  revccat  14467  pwp1fsum  16088  vdwlem8  16677  issubc3  17552  cofucl  17591  catccatid  17809  xpccatid  17893  issstrmgm  18325  mndpropd  18398  issubmnd  18400  pwspjmhm  18456  gsumsgrpccat  18466  gsumccatOLD  18467  smndex1gbas  18529  pwmnd  18564  imasgrp  18679  mulgnndir  18720  subg0cl  18751  subginvcl  18752  subgcl  18753  psgnunilem2  19091  efgsp1  19331  gsumzsubmcl  19507  dpjghm  19654  pwsco1rhm  19970  pwsco2rhm  19971  isdrngd  20004  subrgmcl  20024  subrgunit  20030  issubdrg  20037  lmodprop2d  20173  qsssubdrg  20645  psraddcl  21140  psrmulcllem  21144  psrvscacl  21150  mhppwdeg  21328  matgsum  21574  mat1rhmcl  21618  dmatmulcl  21637  scmatghm  21670  imacmp  22536  prdstps  22768  symgtgp  23245  prdstgpd  23264  tsmssub  23288  ustuqtop3  23383  utop2nei  23390  xpsxmetlem  23520  xpsmet  23523  imasf1oxms  23633  imasf1oms  23634  prdsmslem1  23671  prdsxmslem1  23672  prdsxmslem2  23673  tngngp2  23804  cnmpopc  24079  caublcls  24461  minveclem3a  24579  efsubm  25695  wlkl1loop  27992  wlkres  28025  clwwlknonex2lem1  28457  eucrct2eupth  28595  cyc3co2  31393  drgextlsp  31667  fedgmullem2  31697  cvmliftlem7  33239  cvmliftlem10  33242  ex-sategoelel  33369  ex-sategoelelomsuc  33374  prdsbnd  35937  prdstotbnd  35938  prdsbnd2  35939  cnpwstotbnd  35941  repwsmet  35978  diblss  39170  kelac1  40874  iunrelexpuztr  41286  mnuprdlem3  41851  fnchoice  42531  sumnnodd  43130  sublimc  43152  divlimc  43156  cncfshiftioo  43392  itgperiod  43481  stoweidlem26  43526  dirkercncflem2  43604  fourierdlem32  43639  fourierdlem33  43640  fourierdlem46  43652  fourierdlem48  43654  fourierdlem49  43655  fourierdlem62  43668  fourierdlem74  43680  fourierdlem75  43681  fourierdlem76  43682  fourierdlem81  43687  fourierdlem88  43694  fourierdlem89  43695  fourierdlem91  43697  fourierdlem93  43699  fourierdlem103  43709  fourierdlem104  43710  fouriersw  43731  fouriercn  43732  smfco  44292  uspgropssxp  45262  issubmgm2  45300  rnghmsubcsetclem1  45489  rnghmsubcsetclem2  45490  rngccatidALTV  45503  funcrngcsetc  45512  rhmsubcsetclem1  45535  rhmsubcsetclem2  45536  rhmsubcrngclem1  45541  rhmsubcrngclem2  45542  funcringcsetc  45549  ringccatidALTV  45566  srhmsubc  45590  rhmsubclem3  45602  rhmsubclem4  45603  srhmsubcALTV  45608  rhmsubcALTVlem3  45620  rhmsubcALTVlem4  45621  ovmpordxf  45630  indthinc  46289  indthincALT  46290  mndtccatid  46330