Theorem 3eltr4d 2840

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802

This theorem is referenced by:  elimdelov  7516  ovmpodxf  7571  cantnflt  9697  cantnflem1  9714  cofsmo  10294  cfsmolem  10295  axcclem  10482  smobeth  10611  iccf1o  13508  ccatw2s1p1  14622  revccat  14752  pwp1fsum  16371  vdwlem8  16960  issubc3  17838  cofucl  17877  catccatid  18098  xpccatid  18182  issstrmgm  18616  issubmgm2  18666  sgrppropd  18694  mndpropd  18722  issubmnd  18724  pwspjmhm  18790  gsumsgrpccat  18800  smndex1gbas  18862  pwmnd  18897  imasgrp  19020  mulgnndir  19066  subg0cl  19097  subginvcl  19098  subgcl  19099  psgnunilem2  19462  finodsubmsubg  19534  efgsp1  19704  gsumzsubmcl  19885  dpjghm  20032  pwsco1rhm  20453  pwsco2rhm  20454  subrngmcl  20506  subrgunit  20541  rnghmsubcsetclem1  20576  rnghmsubcsetclem2  20577  funcrngcsetc  20585  rhmsubcsetclem1  20605  rhmsubcsetclem2  20606  rhmsubcrngclem1  20611  rhmsubcrngclem2  20612  funcringcsetc  20619  srhmsubc  20625  rhmsubclem3  20632  rhmsubclem4  20633  isdrngd  20669  isdrngdOLD  20671  issubdrg  20680  lmodprop2d  20819  rngqiprngimfo  21208  qsssubdrg  21376  pzriprnglem4  21427  pzriprnglem5  21428  psraddcl  21900  psraddclOLD  21901  psrmulcllem  21907  psrvscacl  21913  mhppwdeg  22097  psdcl  22108  matgsum  22383  mat1rhmcl  22427  dmatmulcl  22446  scmatghm  22479  imacmp  23345  prdstps  23577  symgtgp  24054  prdstgpd  24073  tsmssub  24097  ustuqtop3  24192  utop2nei  24199  xpsxmetlem  24329  xpsmet  24332  imasf1oxms  24442  imasf1oms  24443  prdsmslem1  24480  prdsxmslem1  24481  prdsxmslem2  24482  tngngp2  24613  cnmpopc  24893  caublcls  25281  minveclem3a  25399  efsubm  26530  noseqrdg0  28230  wlkl1loop  29524  wlkres  29556  clwwlknonex2lem1  29989  eucrct2eupth  30127  cyc3co2  32953  sdrgdvcl  33085  sdrginvcl  33086  drgextlsp  33424  fedgmullem2  33459  algextdeglem4  33519  cvmliftlem7  35032  cvmliftlem10  35035  ex-sategoelel  35162  ex-sategoelelomsuc  35167  prdsbnd  37397  prdstotbnd  37398  prdsbnd2  37399  cnpwstotbnd  37401  repwsmet  37438  diblss  40773  kelac1  42629  omcl2  42904  ofoafg  42925  naddwordnexlem0  42968  naddwordnexlem3  42971  iunrelexpuztr  43291  mnuprdlem3  43853  fnchoice  44533  sumnnodd  45156  sublimc  45178  divlimc  45182  cncfshiftioo  45418  itgperiod  45507  stoweidlem26  45552  dirkercncflem2  45630  fourierdlem32  45665  fourierdlem33  45666  fourierdlem46  45678  fourierdlem48  45680  fourierdlem49  45681  fourierdlem62  45694  fourierdlem74  45706  fourierdlem75  45707  fourierdlem76  45708  fourierdlem81  45713  fourierdlem88  45720  fourierdlem89  45721  fourierdlem91  45723  fourierdlem93  45725  fourierdlem103  45735  fourierdlem104  45736  fouriersw  45757  fouriercn  45758  smfco  46328  uspgropssxp  47392  rngccatidALTV  47520  rhmsubcALTVlem3  47531  rhmsubcALTVlem4  47532  ringccatidALTV  47554  srhmsubcALTV  47573  ovmpordxf  47588  indthinc  48244  indthincALT  48245  mndtccatid  48285