Theorem 3eltr4d 2876

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  elimdelov  7516  ovmpodxf  7570  cantnflt  9673  cantnflem1  9690  cofsmo  10347  cfsmolem  10348  axcclem  10535  smobeth  10671  iccf1o  13627  ccatw2s1p1  14784  revccat  14915  pwp1fsum  16561  vdwlem8  17166  issubc3  18024  cofucl  18063  catccatid  18281  xpccatid  18362  issstrmgm  18831  issubmgm2  18892  sgrppropd  18920  mndpropd  18951  issubmnd  18953  pwspjmhm  19026  gsumsgrpccat  19036  smndex1gbas  19098  smndex1gbasOLD  19099  pwmnd  19143  imasgrp  19266  mulgnndir  19313  subg0cl  19344  subginvcl  19345  subgcl  19346  psgnunilem2  19709  finodsubmsubg  19781  efgsp1  19951  gsumzsubmcl  20132  dpjghm  20279  pwsco1rhm  20741  pwsco2rhm  20742  subrngmcl  20809  subrgunit  20842  rnghmsubcsetclem1  20883  rnghmsubcsetclem2  20884  funcrngcsetc  20892  rhmsubcsetclem1  20912  rhmsubcsetclem2  20913  rhmsubcrngclem1  20918  rhmsubcrngclem2  20919  funcringcsetc  20926  srhmsubc  20932  rhmsubclem3  20939  rhmsubclem4  20940  isdrngd  21022  isdrngdOLD  21024  issubdrg  21037  lmodprop2d  21199  rngqiprngimfo  21597  qsssubdrg  21732  pzriprnglem4  21790  pzriprnglem5  21791  psraddcl  22247  psrmulcllem  22253  psrvscacl  22259  mhppwdeg  22471  psdcl  22482  matgsum  22752  mat1rhmcl  22796  dmatmulcl  22815  scmatghm  22848  imacmp  23715  prdstps  23948  symgtgp  24425  prdstgpd  24444  tsmssub  24468  ustuqtop3  24562  utop2nei  24569  xpsxmetlem  24698  xpsmet  24701  imasf1oxms  24808  imasf1oms  24809  prdsmslem1  24846  prdsxmslem1  24847  prdsxmslem2  24848  tngngp2  24971  cnmpopc  25249  caublcls  25630  minveclem3a  25748  efsubm  26879  negleft  28444  negright  28445  noseqrdg0  28693  angmgmaddov2  29389  wlkl1loop  30218  wlkres  30249  clwwlknonex2lem1  30698  eucrct2eupth  30846  subgmulgcld  33604  cyc3co2  33701  sdrgdvcl  33861  sdrginvcl  33862  drgextlsp  34226  fedgmullem2  34262  algextdeglem4  34352  cvmliftlem7  36056  cvmliftlem10  36059  ex-sategoelel  36186  ex-sategoelelomsuc  36191  nadddilem1  36969  nadddilem2  36970  nadddilem3  36971  nadddilem4  36972  prdsbnd  38727  prdstotbnd  38728  prdsbnd2  38729  cnpwstotbnd  38731  repwsmet  38768  diblss  42227  kelac1  44064  omcl2  44334  ofoafg  44355  naddwordnexlem0  44397  naddwordnexlem3  44400  iunrelexpuztr  44718  mnuprdlem3  45257  fnchoice  46045  sumnnodd  46641  sublimc  46661  divlimc  46665  cncfshiftioo  46901  itgperiod  46990  stoweidlem26  47035  dirkercncflem2  47113  fourierdlem32  47148  fourierdlem33  47149  fourierdlem46  47161  fourierdlem48  47163  fourierdlem49  47164  fourierdlem62  47177  fourierdlem74  47189  fourierdlem75  47190  fourierdlem76  47191  fourierdlem81  47196  fourierdlem88  47203  fourierdlem89  47204  fourierdlem91  47206  fourierdlem93  47208  fourierdlem103  47218  fourierdlem104  47219  fouriersw  47240  fouriercn  47241  smfco  47811  uspgropssxp  49241  rngccatidALTV  49368  rhmsubcALTVlem3  49379  rhmsubcALTVlem4  49380  ringccatidALTV  49402  srhmsubcALTV  49421  ovmpordxf  49450  discsubc  50171  imaf1co  50262  tposcurf2cl  50409  fuco2eld  50420  fuco22natlem  50452  indthinc  50569  indthincALT  50570  mndtccatid  50694