Theorem 3eltr4d 2850

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-clel 2810

This theorem is referenced by:  elimdelov  7508  ovmpodxf  7562  cantnflt  9691  cantnflem1  9708  cofsmo  10288  cfsmolem  10289  axcclem  10476  smobeth  10605  iccf1o  13518  ccatw2s1p1  14659  revccat  14789  pwp1fsum  16415  vdwlem8  17013  issubc3  17867  cofucl  17906  catccatid  18124  xpccatid  18205  issstrmgm  18636  issubmgm2  18686  sgrppropd  18714  mndpropd  18742  issubmnd  18744  pwspjmhm  18813  gsumsgrpccat  18823  smndex1gbas  18885  pwmnd  18920  imasgrp  19044  mulgnndir  19091  subg0cl  19122  subginvcl  19123  subgcl  19124  psgnunilem2  19481  finodsubmsubg  19553  efgsp1  19723  gsumzsubmcl  19904  dpjghm  20051  pwsco1rhm  20467  pwsco2rhm  20468  subrngmcl  20522  subrgunit  20555  rnghmsubcsetclem1  20596  rnghmsubcsetclem2  20597  funcrngcsetc  20605  rhmsubcsetclem1  20625  rhmsubcsetclem2  20626  rhmsubcrngclem1  20631  rhmsubcrngclem2  20632  funcringcsetc  20639  srhmsubc  20645  rhmsubclem3  20652  rhmsubclem4  20653  isdrngd  20730  isdrngdOLD  20732  issubdrg  20745  lmodprop2d  20886  rngqiprngimfo  21267  qsssubdrg  21399  pzriprnglem4  21450  pzriprnglem5  21451  psraddcl  21903  psraddclOLD  21904  psrmulcllem  21910  psrvscacl  21916  mhppwdeg  22093  psdcl  22104  matgsum  22380  mat1rhmcl  22424  dmatmulcl  22443  scmatghm  22476  imacmp  23340  prdstps  23572  symgtgp  24049  prdstgpd  24068  tsmssub  24092  ustuqtop3  24187  utop2nei  24194  xpsxmetlem  24323  xpsmet  24326  imasf1oxms  24433  imasf1oms  24434  prdsmslem1  24471  prdsxmslem1  24472  prdsxmslem2  24473  tngngp2  24596  cnmpopc  24878  caublcls  25266  minveclem3a  25384  efsubm  26517  noseqrdg0  28258  wlkl1loop  29623  wlkres  29655  clwwlknonex2lem1  30093  eucrct2eupth  30231  subgmulgcld  33043  cyc3co2  33156  sdrgdvcl  33298  sdrginvcl  33299  drgextlsp  33638  fedgmullem2  33675  algextdeglem4  33759  cvmliftlem7  35318  cvmliftlem10  35321  ex-sategoelel  35448  ex-sategoelelomsuc  35453  prdsbnd  37822  prdstotbnd  37823  prdsbnd2  37824  cnpwstotbnd  37826  repwsmet  37863  diblss  41194  kelac1  43054  omcl2  43324  ofoafg  43345  naddwordnexlem0  43387  naddwordnexlem3  43390  iunrelexpuztr  43710  mnuprdlem3  44265  fnchoice  45020  sumnnodd  45626  sublimc  45648  divlimc  45652  cncfshiftioo  45888  itgperiod  45977  stoweidlem26  46022  dirkercncflem2  46100  fourierdlem32  46135  fourierdlem33  46136  fourierdlem46  46148  fourierdlem48  46150  fourierdlem49  46151  fourierdlem62  46164  fourierdlem74  46176  fourierdlem75  46177  fourierdlem76  46178  fourierdlem81  46183  fourierdlem88  46190  fourierdlem89  46191  fourierdlem91  46193  fourierdlem93  46195  fourierdlem103  46205  fourierdlem104  46206  fouriersw  46227  fouriercn  46228  smfco  46798  uspgropssxp  48086  rngccatidALTV  48214  rhmsubcALTVlem3  48225  rhmsubcALTVlem4  48226  ringccatidALTV  48248  srhmsubcALTV  48267  ovmpordxf  48281  discsubc  48998  imaf1co  49062  tposcurf2cl  49180  fuco2eld  49191  fuco22natlem  49223  indthinc  49315  indthincALT  49316  mndtccatid  49431