Theorem 3eltr4d 2878

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2838

This theorem is used by:  elimdelov  7523  ovmpodxf  7577  cantnflt  9683  cantnflem1  9700  cofsmo  10357  cfsmolem  10358  axcclem  10545  smobeth  10681  iccf1o  13637  ccatw2s1p1  14795  revccat  14926  pwp1fsum  16573  vdwlem8  17178  issubc3  18036  cofucl  18075  catccatid  18293  xpccatid  18374  issstrmgm  18843  issubmgm2  18904  sgrppropd  18932  mndpropd  18963  issubmnd  18965  pwspjmhm  19038  gsumsgrpccat  19048  smndex1gbas  19110  smndex1gbasOLD  19111  pwmnd  19155  imasgrp  19278  mulgnndir  19325  subg0cl  19356  subginvcl  19357  subgcl  19358  psgnunilem2  19721  finodsubmsubg  19793  efgsp1  19963  gsumzsubmcl  20144  dpjghm  20291  pwsco1rhm  20753  pwsco2rhm  20754  subrngmcl  20821  subrgunit  20854  rnghmsubcsetclem1  20895  rnghmsubcsetclem2  20896  funcrngcsetc  20904  rhmsubcsetclem1  20924  rhmsubcsetclem2  20925  rhmsubcrngclem1  20930  rhmsubcrngclem2  20931  funcringcsetc  20938  srhmsubc  20944  rhmsubclem3  20951  rhmsubclem4  20952  isdrngd  21034  isdrngdOLD  21036  issubdrg  21049  lmodprop2d  21211  rngqiprngimfo  21609  qsssubdrg  21744  pzriprnglem4  21802  pzriprnglem5  21803  psraddcl  22259  psrmulcllem  22265  psrvscacl  22271  mhppwdeg  22483  psdcl  22494  matgsum  22764  mat1rhmcl  22808  dmatmulcl  22827  scmatghm  22860  imacmp  23727  prdstps  23960  symgtgp  24437  prdstgpd  24456  tsmssub  24480  ustuqtop3  24574  utop2nei  24581  xpsxmetlem  24710  xpsmet  24713  imasf1oxms  24820  imasf1oms  24821  prdsmslem1  24858  prdsxmslem1  24859  prdsxmslem2  24860  tngngp2  24983  cnmpopc  25261  caublcls  25642  minveclem3a  25760  efsubm  26891  negleft  28456  negright  28457  noseqrdg0  28705  angmgmaddov2  29401  wlkl1loop  30230  wlkres  30261  clwwlknonex2lem1  30710  eucrct2eupth  30858  subgmulgcld  33657  cyc3co2  33754  sdrgdvcl  33914  sdrginvcl  33915  drgextlsp  34279  fedgmullem2  34315  algextdeglem4  34405  cvmliftlem7  36177  cvmliftlem10  36180  ex-sategoelel  36307  ex-sategoelelomsuc  36312  nadddilem1  37096  nadddilem2  37097  nadddilem3  37098  nadddilem4  37099  prdsbnd  38867  prdstotbnd  38868  prdsbnd2  38869  cnpwstotbnd  38871  repwsmet  38908  diblss  42367  kelac1  44205  omcl2  44475  ofoafg  44496  naddwordnexlem0  44538  naddwordnexlem3  44541  iunrelexpuztr  44859  mnuprdlem3  45398  fnchoice  46185  sumnnodd  46781  sublimc  46801  divlimc  46805  cncfshiftioo  47041  itgperiod  47130  stoweidlem26  47175  dirkercncflem2  47253  fourierdlem32  47288  fourierdlem33  47289  fourierdlem46  47301  fourierdlem48  47303  fourierdlem49  47304  fourierdlem62  47317  fourierdlem74  47329  fourierdlem75  47330  fourierdlem76  47331  fourierdlem81  47336  fourierdlem88  47343  fourierdlem89  47344  fourierdlem91  47346  fourierdlem93  47348  fourierdlem103  47358  fourierdlem104  47359  fouriersw  47380  fouriercn  47381  smfco  47951  uspgropssxp  49381  rngccatidALTV  49508  rhmsubcALTVlem3  49519  rhmsubcALTVlem4  49520  ringccatidALTV  49542  srhmsubcALTV  49561  ovmpordxf  49590  discsubc  50317  imaf1co  50410  tposcurf2cl  50563  fuco2eld  50574  fuco22natlem  50606  indthinc  50736  indthincALT  50737  mndtccatid  50864  parhomco2  50899  parhomco  50900