Theorem 3eltr4d 2884

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  elimdelov  7507  ovmpodxf  7561  cantnflt  9640  cantnflem1  9657  cofsmo  10252  cfsmolem  10253  axcclem  10440  smobeth  10570  iccf1o  13522  ccatw2s1p1  14673  revccat  14802  pwp1fsum  16448  vdwlem8  17047  issubc3  17905  cofucl  17944  catccatid  18162  xpccatid  18243  issstrmgm  18710  issubmgm2  18760  sgrppropd  18788  mndpropd  18816  issubmnd  18818  pwspjmhm  18888  gsumsgrpccat  18898  smndex1gbas  18960  smndex1gbasOLD  18961  pwmnd  18998  imasgrp  19121  mulgnndir  19168  subg0cl  19199  subginvcl  19200  subgcl  19201  psgnunilem2  19564  finodsubmsubg  19636  efgsp1  19806  gsumzsubmcl  19987  dpjghm  20134  pwsco1rhm  20583  pwsco2rhm  20584  subrngmcl  20641  subrgunit  20674  rnghmsubcsetclem1  20715  rnghmsubcsetclem2  20716  funcrngcsetc  20724  rhmsubcsetclem1  20744  rhmsubcsetclem2  20745  rhmsubcrngclem1  20750  rhmsubcrngclem2  20751  funcringcsetc  20758  srhmsubc  20764  rhmsubclem3  20771  rhmsubclem4  20772  isdrngd  20846  isdrngdOLD  20848  issubdrg  20860  lmodprop2d  21022  rngqiprngimfo  21411  qsssubdrg  21544  pzriprnglem4  21602  pzriprnglem5  21603  psraddcl  22057  psrmulcllem  22063  psrvscacl  22069  mhppwdeg  22281  psdcl  22292  matgsum  22562  mat1rhmcl  22606  dmatmulcl  22625  scmatghm  22658  imacmp  23522  prdstps  23754  symgtgp  24231  prdstgpd  24250  tsmssub  24274  ustuqtop3  24368  utop2nei  24375  xpsxmetlem  24504  xpsmet  24507  imasf1oxms  24614  imasf1oms  24615  prdsmslem1  24652  prdsxmslem1  24653  prdsxmslem2  24654  tngngp2  24777  cnmpopc  25055  caublcls  25436  minveclem3a  25554  efsubm  26681  negleft  28216  negright  28217  noseqrdg0  28465  wlkl1loop  29927  wlkres  29958  clwwlknonex2lem1  30398  eucrct2eupth  30536  subgmulgcld  33303  cyc3co2  33400  sdrgdvcl  33562  sdrginvcl  33563  drgextlsp  33928  fedgmullem2  33964  algextdeglem4  34054  cvmliftlem7  35681  cvmliftlem10  35684  ex-sategoelel  35811  ex-sategoelelomsuc  35816  prdsbnd  38331  prdstotbnd  38332  prdsbnd2  38333  cnpwstotbnd  38335  repwsmet  38372  diblss  41833  kelac1  43681  omcl2  43951  ofoafg  43972  naddwordnexlem0  44014  naddwordnexlem3  44017  iunrelexpuztr  44336  mnuprdlem3  44875  fnchoice  45640  sumnnodd  46237  sublimc  46257  divlimc  46261  cncfshiftioo  46497  itgperiod  46586  stoweidlem26  46631  dirkercncflem2  46709  fourierdlem32  46744  fourierdlem33  46745  fourierdlem46  46757  fourierdlem48  46759  fourierdlem49  46760  fourierdlem62  46773  fourierdlem74  46785  fourierdlem75  46786  fourierdlem76  46787  fourierdlem81  46792  fourierdlem88  46799  fourierdlem89  46800  fourierdlem91  46802  fourierdlem93  46804  fourierdlem103  46814  fourierdlem104  46815  fouriersw  46836  fouriercn  46837  smfco  47407  uspgropssxp  48797  rngccatidALTV  48925  rhmsubcALTVlem3  48936  rhmsubcALTVlem4  48937  ringccatidALTV  48959  srhmsubcALTV  48978  ovmpordxf  49003  discsubc  49726  imaf1co  49817  tposcurf2cl  49964  fuco2eld  49975  fuco22natlem  50007  indthinc  50124  indthincALT  50125  mndtccatid  50249