Theorem 3eltr4d 2859

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  elimdelov  7546  ovmpodxf  7600  cantnflt  9741  cantnflem1  9758  cofsmo  10338  cfsmolem  10339  axcclem  10526  smobeth  10655  iccf1o  13556  ccatw2s1p1  14684  revccat  14814  pwp1fsum  16439  vdwlem8  17035  issubc3  17913  cofucl  17952  catccatid  18173  xpccatid  18257  issstrmgm  18691  issubmgm2  18741  sgrppropd  18769  mndpropd  18797  issubmnd  18799  pwspjmhm  18865  gsumsgrpccat  18875  smndex1gbas  18937  pwmnd  18972  imasgrp  19096  mulgnndir  19143  subg0cl  19174  subginvcl  19175  subgcl  19176  psgnunilem2  19537  finodsubmsubg  19609  efgsp1  19779  gsumzsubmcl  19960  dpjghm  20107  pwsco1rhm  20528  pwsco2rhm  20529  subrngmcl  20583  subrgunit  20618  rnghmsubcsetclem1  20653  rnghmsubcsetclem2  20654  funcrngcsetc  20662  rhmsubcsetclem1  20682  rhmsubcsetclem2  20683  rhmsubcrngclem1  20688  rhmsubcrngclem2  20689  funcringcsetc  20696  srhmsubc  20702  rhmsubclem3  20709  rhmsubclem4  20710  isdrngd  20787  isdrngdOLD  20789  issubdrg  20803  lmodprop2d  20944  rngqiprngimfo  21334  qsssubdrg  21467  pzriprnglem4  21518  pzriprnglem5  21519  psraddcl  21981  psraddclOLD  21982  psrmulcllem  21988  psrvscacl  21994  mhppwdeg  22177  psdcl  22188  matgsum  22464  mat1rhmcl  22508  dmatmulcl  22527  scmatghm  22560  imacmp  23426  prdstps  23658  symgtgp  24135  prdstgpd  24154  tsmssub  24178  ustuqtop3  24273  utop2nei  24280  xpsxmetlem  24410  xpsmet  24413  imasf1oxms  24523  imasf1oms  24524  prdsmslem1  24561  prdsxmslem1  24562  prdsxmslem2  24563  tngngp2  24694  cnmpopc  24974  caublcls  25362  minveclem3a  25480  efsubm  26611  noseqrdg0  28331  wlkl1loop  29674  wlkres  29706  clwwlknonex2lem1  30139  eucrct2eupth  30277  cyc3co2  33133  sdrgdvcl  33266  sdrginvcl  33267  drgextlsp  33608  fedgmullem2  33643  algextdeglem4  33711  cvmliftlem7  35259  cvmliftlem10  35262  ex-sategoelel  35389  ex-sategoelelomsuc  35394  prdsbnd  37753  prdstotbnd  37754  prdsbnd2  37755  cnpwstotbnd  37757  repwsmet  37794  diblss  41127  kelac1  43020  omcl2  43295  ofoafg  43316  naddwordnexlem0  43358  naddwordnexlem3  43361  iunrelexpuztr  43681  mnuprdlem3  44243  fnchoice  44929  sumnnodd  45551  sublimc  45573  divlimc  45577  cncfshiftioo  45813  itgperiod  45902  stoweidlem26  45947  dirkercncflem2  46025  fourierdlem32  46060  fourierdlem33  46061  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem62  46089  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem81  46108  fourierdlem88  46115  fourierdlem89  46116  fourierdlem91  46118  fourierdlem93  46120  fourierdlem103  46130  fourierdlem104  46131  fouriersw  46152  fouriercn  46153  smfco  46723  uspgropssxp  47867  rngccatidALTV  47995  rhmsubcALTVlem3  48006  rhmsubcALTVlem4  48007  ringccatidALTV  48029  srhmsubcALTV  48048  ovmpordxf  48063  indthinc  48719  indthincALT  48720  mndtccatid  48760