Theorem 3eltr4d 2846

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 2834	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
5	1, 4	eqeltrd 2831	1 ⊢ (𝜑 → 𝐶 ∈ 𝐷)

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-clel 2809

This theorem is referenced by:  elimdelov  7285  ovmpodxf  7337  cantnflt  9265  cantnflem1  9282  cofsmo  9848  cfsmolem  9849  axcclem  10036  smobeth  10165  iccf1o  13049  ccatw2s1p1  14163  ccatw2s1p1OLD  14164  revccat  14296  pwp1fsum  15915  vdwlem8  16504  issubc3  17309  cofucl  17348  catccatid  17566  xpccatid  17649  issstrmgm  18079  mndpropd  18152  issubmnd  18154  pwspjmhm  18210  gsumsgrpccat  18220  gsumccatOLD  18221  smndex1gbas  18283  pwmnd  18318  imasgrp  18433  mulgnndir  18474  subg0cl  18505  subginvcl  18506  subgcl  18507  psgnunilem2  18841  efgsp1  19081  gsumzsubmcl  19257  dpjghm  19404  pwsco1rhm  19712  pwsco2rhm  19713  isdrngd  19746  subrgmcl  19766  subrgunit  19772  issubdrg  19779  lmodprop2d  19915  qsssubdrg  20376  psraddcl  20862  psrmulcllem  20866  psrvscacl  20872  mhppwdeg  21044  matgsum  21288  mat1rhmcl  21332  dmatmulcl  21351  scmatghm  21384  imacmp  22248  prdstps  22480  symgtgp  22957  prdstgpd  22976  tsmssub  23000  ustuqtop3  23095  utop2nei  23102  xpsxmetlem  23231  xpsmet  23234  imasf1oxms  23341  imasf1oms  23342  prdsmslem1  23379  prdsxmslem1  23380  prdsxmslem2  23381  tngngp2  23504  cnmpopc  23779  caublcls  24160  minveclem3a  24278  efsubm  25394  wlkl1loop  27679  wlkres  27712  clwwlknonex2lem1  28144  eucrct2eupth  28282  cyc3co2  31080  drgextlsp  31349  fedgmullem2  31379  cvmliftlem7  32920  cvmliftlem10  32923  ex-sategoelel  33050  ex-sategoelelomsuc  33055  prdsbnd  35637  prdstotbnd  35638  prdsbnd2  35639  cnpwstotbnd  35641  repwsmet  35678  diblss  38870  kelac1  40532  iunrelexpuztr  40945  mnuprdlem3  41506  fnchoice  42186  sumnnodd  42789  sublimc  42811  divlimc  42815  cncfshiftioo  43051  itgperiod  43140  stoweidlem26  43185  dirkercncflem2  43263  fourierdlem32  43298  fourierdlem33  43299  fourierdlem46  43311  fourierdlem48  43313  fourierdlem49  43314  fourierdlem62  43327  fourierdlem74  43339  fourierdlem75  43340  fourierdlem76  43341  fourierdlem81  43346  fourierdlem88  43353  fourierdlem89  43354  fourierdlem91  43356  fourierdlem93  43358  fourierdlem103  43368  fourierdlem104  43369  fouriersw  43390  fouriercn  43391  smfco  43951  uspgropssxp  44922  issubmgm2  44960  rnghmsubcsetclem1  45149  rnghmsubcsetclem2  45150  rngccatidALTV  45163  funcrngcsetc  45172  rhmsubcsetclem1  45195  rhmsubcsetclem2  45196  rhmsubcrngclem1  45201  rhmsubcrngclem2  45202  funcringcsetc  45209  ringccatidALTV  45226  srhmsubc  45250  rhmsubclem3  45262  rhmsubclem4  45263  srhmsubcALTV  45268  rhmsubcALTVlem3  45280  rhmsubcALTVlem4  45281  ovmpordxf  45290  indthinc  45949  indthincALT  45950  mndtccatid  45988