Theorem 3eltr4d 2877

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837

This theorem is referenced by:  elimdelov  7492  ovmpodxf  7546  cantnflt  9627  cantnflem1  9644  cofsmo  10226  cfsmolem  10227  axcclem  10414  smobeth  10544  iccf1o  13500  ccatw2s1p1  14650  revccat  14779  pwp1fsum  16425  vdwlem8  17024  issubc3  17882  cofucl  17921  catccatid  18139  xpccatid  18220  issstrmgm  18687  issubmgm2  18737  sgrppropd  18765  mndpropd  18793  issubmnd  18795  pwspjmhm  18864  gsumsgrpccat  18874  smndex1gbas  18936  smndex1gbasOLD  18937  pwmnd  18974  imasgrp  19098  mulgnndir  19145  subg0cl  19176  subginvcl  19177  subgcl  19178  psgnunilem2  19535  finodsubmsubg  19607  efgsp1  19777  gsumzsubmcl  19958  dpjghm  20105  pwsco1rhm  20551  pwsco2rhm  20552  subrngmcl  20607  subrgunit  20640  rnghmsubcsetclem1  20681  rnghmsubcsetclem2  20682  funcrngcsetc  20690  rhmsubcsetclem1  20710  rhmsubcsetclem2  20711  rhmsubcrngclem1  20716  rhmsubcrngclem2  20717  funcringcsetc  20724  srhmsubc  20730  rhmsubclem3  20737  rhmsubclem4  20738  isdrngd  20815  isdrngdOLD  20817  issubdrg  20829  lmodprop2d  20991  rngqiprngimfo  21371  qsssubdrg  21478  pzriprnglem4  21536  pzriprnglem5  21537  psraddcl  21991  psrmulcllem  21997  psrvscacl  22003  mhppwdeg  22215  psdcl  22226  matgsum  22497  mat1rhmcl  22541  dmatmulcl  22560  scmatghm  22593  imacmp  23457  prdstps  23689  symgtgp  24166  prdstgpd  24185  tsmssub  24209  ustuqtop3  24303  utop2nei  24310  xpsxmetlem  24439  xpsmet  24442  imasf1oxms  24549  imasf1oms  24550  prdsmslem1  24587  prdsxmslem1  24588  prdsxmslem2  24589  tngngp2  24712  cnmpopc  24990  caublcls  25371  minveclem3a  25489  efsubm  26616  negleft  28151  negright  28152  noseqrdg0  28400  wlkl1loop  29838  wlkres  29869  clwwlknonex2lem1  30309  eucrct2eupth  30447  subgmulgcld  33223  cyc3co2  33320  sdrgdvcl  33486  sdrginvcl  33487  drgextlsp  33891  fedgmullem2  33927  algextdeglem4  34017  cvmliftlem7  35641  cvmliftlem10  35644  ex-sategoelel  35771  ex-sategoelelomsuc  35776  prdsbnd  38292  prdstotbnd  38293  prdsbnd2  38294  cnpwstotbnd  38296  repwsmet  38333  diblss  41794  kelac1  43640  omcl2  43910  ofoafg  43931  naddwordnexlem0  43973  naddwordnexlem3  43976  iunrelexpuztr  44295  mnuprdlem3  44850  fnchoice  45609  sumnnodd  46206  sublimc  46226  divlimc  46230  cncfshiftioo  46466  itgperiod  46555  stoweidlem26  46600  dirkercncflem2  46678  fourierdlem32  46713  fourierdlem33  46714  fourierdlem46  46726  fourierdlem48  46728  fourierdlem49  46729  fourierdlem62  46742  fourierdlem74  46754  fourierdlem75  46755  fourierdlem76  46756  fourierdlem81  46761  fourierdlem88  46768  fourierdlem89  46769  fourierdlem91  46771  fourierdlem93  46773  fourierdlem103  46783  fourierdlem104  46784  fouriersw  46805  fouriercn  46806  smfco  47376  uspgropssxp  48766  rngccatidALTV  48894  rhmsubcALTVlem3  48905  rhmsubcALTVlem4  48906  ringccatidALTV  48928  srhmsubcALTV  48947  ovmpordxf  48961  discsubc  49685  imaf1co  49776  tposcurf2cl  49923  fuco2eld  49934  fuco22natlem  49966  indthinc  50083  indthincALT  50084  mndtccatid  50208