Theorem 3eltr4d 2855

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731  df-clel 2817

This theorem is referenced by:  elimdelov  7362  ovmpodxf  7414  cantnflt  9391  cantnflem1  9408  cofsmo  10009  cfsmolem  10010  axcclem  10197  smobeth  10326  iccf1o  13210  ccatw2s1p1  14327  ccatw2s1p1OLD  14328  revccat  14460  pwp1fsum  16081  vdwlem8  16670  issubc3  17545  cofucl  17584  catccatid  17802  xpccatid  17886  issstrmgm  18318  mndpropd  18391  issubmnd  18393  pwspjmhm  18449  gsumsgrpccat  18459  gsumccatOLD  18460  smndex1gbas  18522  pwmnd  18557  imasgrp  18672  mulgnndir  18713  subg0cl  18744  subginvcl  18745  subgcl  18746  psgnunilem2  19084  efgsp1  19324  gsumzsubmcl  19500  dpjghm  19647  pwsco1rhm  19963  pwsco2rhm  19964  isdrngd  19997  subrgmcl  20017  subrgunit  20023  issubdrg  20030  lmodprop2d  20166  qsssubdrg  20638  psraddcl  21133  psrmulcllem  21137  psrvscacl  21143  mhppwdeg  21321  matgsum  21567  mat1rhmcl  21611  dmatmulcl  21630  scmatghm  21663  imacmp  22529  prdstps  22761  symgtgp  23238  prdstgpd  23257  tsmssub  23281  ustuqtop3  23376  utop2nei  23383  xpsxmetlem  23513  xpsmet  23516  imasf1oxms  23626  imasf1oms  23627  prdsmslem1  23664  prdsxmslem1  23665  prdsxmslem2  23666  tngngp2  23797  cnmpopc  24072  caublcls  24454  minveclem3a  24572  efsubm  25688  wlkl1loop  27985  wlkres  28018  clwwlknonex2lem1  28450  eucrct2eupth  28588  cyc3co2  31386  drgextlsp  31660  fedgmullem2  31690  cvmliftlem7  33232  cvmliftlem10  33235  ex-sategoelel  33362  ex-sategoelelomsuc  33367  prdsbnd  35930  prdstotbnd  35931  prdsbnd2  35932  cnpwstotbnd  35934  repwsmet  35971  diblss  39163  kelac1  40868  iunrelexpuztr  41280  mnuprdlem3  41845  fnchoice  42525  sumnnodd  43125  sublimc  43147  divlimc  43151  cncfshiftioo  43387  itgperiod  43476  stoweidlem26  43521  dirkercncflem2  43599  fourierdlem32  43634  fourierdlem33  43635  fourierdlem46  43647  fourierdlem48  43649  fourierdlem49  43650  fourierdlem62  43663  fourierdlem74  43675  fourierdlem75  43676  fourierdlem76  43677  fourierdlem81  43682  fourierdlem88  43689  fourierdlem89  43690  fourierdlem91  43692  fourierdlem93  43694  fourierdlem103  43704  fourierdlem104  43705  fouriersw  43726  fouriercn  43727  smfco  44287  uspgropssxp  45258  issubmgm2  45296  rnghmsubcsetclem1  45485  rnghmsubcsetclem2  45486  rngccatidALTV  45499  funcrngcsetc  45508  rhmsubcsetclem1  45531  rhmsubcsetclem2  45532  rhmsubcrngclem1  45537  rhmsubcrngclem2  45538  funcringcsetc  45545  ringccatidALTV  45562  srhmsubc  45586  rhmsubclem3  45598  rhmsubclem4  45599  srhmsubcALTV  45604  rhmsubcALTVlem3  45616  rhmsubcALTVlem4  45617  ovmpordxf  45626  indthinc  46285  indthincALT  46286  mndtccatid  46326