Theorem 3eltr4d 2856

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  elimdelov  7529  ovmpodxf  7583  cantnflt  9712  cantnflem1  9729  cofsmo  10309  cfsmolem  10310  axcclem  10497  smobeth  10626  iccf1o  13536  ccatw2s1p1  14674  revccat  14804  pwp1fsum  16428  vdwlem8  17026  issubc3  17894  cofucl  17933  catccatid  18151  xpccatid  18233  issstrmgm  18666  issubmgm2  18716  sgrppropd  18744  mndpropd  18772  issubmnd  18774  pwspjmhm  18843  gsumsgrpccat  18853  smndex1gbas  18915  pwmnd  18950  imasgrp  19074  mulgnndir  19121  subg0cl  19152  subginvcl  19153  subgcl  19154  psgnunilem2  19513  finodsubmsubg  19585  efgsp1  19755  gsumzsubmcl  19936  dpjghm  20083  pwsco1rhm  20502  pwsco2rhm  20503  subrngmcl  20557  subrgunit  20590  rnghmsubcsetclem1  20631  rnghmsubcsetclem2  20632  funcrngcsetc  20640  rhmsubcsetclem1  20660  rhmsubcsetclem2  20661  rhmsubcrngclem1  20666  rhmsubcrngclem2  20667  funcringcsetc  20674  srhmsubc  20680  rhmsubclem3  20687  rhmsubclem4  20688  isdrngd  20765  isdrngdOLD  20767  issubdrg  20781  lmodprop2d  20922  rngqiprngimfo  21311  qsssubdrg  21444  pzriprnglem4  21495  pzriprnglem5  21496  psraddcl  21958  psraddclOLD  21959  psrmulcllem  21965  psrvscacl  21971  mhppwdeg  22154  psdcl  22165  matgsum  22443  mat1rhmcl  22487  dmatmulcl  22506  scmatghm  22539  imacmp  23405  prdstps  23637  symgtgp  24114  prdstgpd  24133  tsmssub  24157  ustuqtop3  24252  utop2nei  24259  xpsxmetlem  24389  xpsmet  24392  imasf1oxms  24502  imasf1oms  24503  prdsmslem1  24540  prdsxmslem1  24541  prdsxmslem2  24542  tngngp2  24673  cnmpopc  24955  caublcls  25343  minveclem3a  25461  efsubm  26593  noseqrdg0  28313  wlkl1loop  29656  wlkres  29688  clwwlknonex2lem1  30126  eucrct2eupth  30264  subgmulgcld  33048  cyc3co2  33160  sdrgdvcl  33301  sdrginvcl  33302  drgextlsp  33644  fedgmullem2  33681  algextdeglem4  33761  cvmliftlem7  35296  cvmliftlem10  35299  ex-sategoelel  35426  ex-sategoelelomsuc  35431  prdsbnd  37800  prdstotbnd  37801  prdsbnd2  37802  cnpwstotbnd  37804  repwsmet  37841  diblss  41172  kelac1  43075  omcl2  43346  ofoafg  43367  naddwordnexlem0  43409  naddwordnexlem3  43412  iunrelexpuztr  43732  mnuprdlem3  44293  fnchoice  45034  sumnnodd  45645  sublimc  45667  divlimc  45671  cncfshiftioo  45907  itgperiod  45996  stoweidlem26  46041  dirkercncflem2  46119  fourierdlem32  46154  fourierdlem33  46155  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem62  46183  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem81  46202  fourierdlem88  46209  fourierdlem89  46210  fourierdlem91  46212  fourierdlem93  46214  fourierdlem103  46224  fourierdlem104  46225  fouriersw  46246  fouriercn  46247  smfco  46817  uspgropssxp  48060  rngccatidALTV  48188  rhmsubcALTVlem3  48199  rhmsubcALTVlem4  48200  ringccatidALTV  48222  srhmsubcALTV  48241  ovmpordxf  48255  tposcurf2cl  49002  fuco2eld  49008  fuco22natlem  49040  indthinc  49109  indthincALT  49110  mndtccatid  49184