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 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  elimdelov  7442  ovmpodxf  7496  cantnflt  9562  cantnflem1  9579  cofsmo  10160  cfsmolem  10161  axcclem  10348  smobeth  10477  iccf1o  13396  ccatw2s1p1  14544  revccat  14673  pwp1fsum  16302  vdwlem8  16900  issubc3  17756  cofucl  17795  catccatid  18013  xpccatid  18094  issstrmgm  18561  issubmgm2  18611  sgrppropd  18639  mndpropd  18667  issubmnd  18669  pwspjmhm  18738  gsumsgrpccat  18748  smndex1gbas  18810  pwmnd  18845  imasgrp  18969  mulgnndir  19016  subg0cl  19047  subginvcl  19048  subgcl  19049  psgnunilem2  19407  finodsubmsubg  19479  efgsp1  19649  gsumzsubmcl  19830  dpjghm  19977  pwsco1rhm  20417  pwsco2rhm  20418  subrngmcl  20472  subrgunit  20505  rnghmsubcsetclem1  20546  rnghmsubcsetclem2  20547  funcrngcsetc  20555  rhmsubcsetclem1  20575  rhmsubcsetclem2  20576  rhmsubcrngclem1  20581  rhmsubcrngclem2  20582  funcringcsetc  20589  srhmsubc  20595  rhmsubclem3  20602  rhmsubclem4  20603  isdrngd  20680  isdrngdOLD  20682  issubdrg  20695  lmodprop2d  20857  rngqiprngimfo  21238  qsssubdrg  21363  pzriprnglem4  21421  pzriprnglem5  21422  psraddcl  21875  psraddclOLD  21876  psrmulcllem  21882  psrvscacl  21888  mhppwdeg  22065  psdcl  22076  matgsum  22352  mat1rhmcl  22396  dmatmulcl  22415  scmatghm  22448  imacmp  23312  prdstps  23544  symgtgp  24021  prdstgpd  24040  tsmssub  24064  ustuqtop3  24158  utop2nei  24165  xpsxmetlem  24294  xpsmet  24297  imasf1oxms  24404  imasf1oms  24405  prdsmslem1  24442  prdsxmslem1  24443  prdsxmslem2  24444  tngngp2  24567  cnmpopc  24849  caublcls  25236  minveclem3a  25354  efsubm  26487  noseqrdg0  28237  wlkl1loop  29616  wlkres  29647  clwwlknonex2lem1  30087  eucrct2eupth  30225  subgmulgcld  33024  cyc3co2  33109  sdrgdvcl  33265  sdrginvcl  33266  drgextlsp  33606  fedgmullem2  33643  algextdeglem4  33733  cvmliftlem7  35335  cvmliftlem10  35338  ex-sategoelel  35465  ex-sategoelelomsuc  35470  prdsbnd  37843  prdstotbnd  37844  prdsbnd2  37845  cnpwstotbnd  37847  repwsmet  37884  diblss  41279  kelac1  43166  omcl2  43436  ofoafg  43457  naddwordnexlem0  43499  naddwordnexlem3  43502  iunrelexpuztr  43822  mnuprdlem3  44377  fnchoice  45136  sumnnodd  45740  sublimc  45760  divlimc  45764  cncfshiftioo  46000  itgperiod  46089  stoweidlem26  46134  dirkercncflem2  46212  fourierdlem32  46247  fourierdlem33  46248  fourierdlem46  46260  fourierdlem48  46262  fourierdlem49  46263  fourierdlem62  46276  fourierdlem74  46288  fourierdlem75  46289  fourierdlem76  46290  fourierdlem81  46295  fourierdlem88  46302  fourierdlem89  46303  fourierdlem91  46305  fourierdlem93  46307  fourierdlem103  46317  fourierdlem104  46318  fouriersw  46339  fouriercn  46340  smfco  46910  uspgropssxp  48254  rngccatidALTV  48382  rhmsubcALTVlem3  48393  rhmsubcALTVlem4  48394  ringccatidALTV  48416  srhmsubcALTV  48435  ovmpordxf  48449  discsubc  49175  imaf1co  49266  tposcurf2cl  49413  fuco2eld  49424  fuco22natlem  49456  indthinc  49573  indthincALT  49574  mndtccatid  49698