Theorem 3eltr4d 2852

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  elimdelov  7464  ovmpodxf  7518  cantnflt  9593  cantnflem1  9610  cofsmo  10191  cfsmolem  10192  axcclem  10379  smobeth  10509  iccf1o  13424  ccatw2s1p1  14572  revccat  14701  pwp1fsum  16330  vdwlem8  16928  issubc3  17785  cofucl  17824  catccatid  18042  xpccatid  18123  issstrmgm  18590  issubmgm2  18640  sgrppropd  18668  mndpropd  18696  issubmnd  18698  pwspjmhm  18767  gsumsgrpccat  18777  smndex1gbas  18839  pwmnd  18874  imasgrp  18998  mulgnndir  19045  subg0cl  19076  subginvcl  19077  subgcl  19078  psgnunilem2  19436  finodsubmsubg  19508  efgsp1  19678  gsumzsubmcl  19859  dpjghm  20006  pwsco1rhm  20447  pwsco2rhm  20448  subrngmcl  20502  subrgunit  20535  rnghmsubcsetclem1  20576  rnghmsubcsetclem2  20577  funcrngcsetc  20585  rhmsubcsetclem1  20605  rhmsubcsetclem2  20606  rhmsubcrngclem1  20611  rhmsubcrngclem2  20612  funcringcsetc  20619  srhmsubc  20625  rhmsubclem3  20632  rhmsubclem4  20633  isdrngd  20710  isdrngdOLD  20712  issubdrg  20725  lmodprop2d  20887  rngqiprngimfo  21268  qsssubdrg  21393  pzriprnglem4  21451  pzriprnglem5  21452  psraddcl  21906  psraddclOLD  21907  psrmulcllem  21913  psrvscacl  21919  mhppwdeg  22105  psdcl  22116  matgsum  22393  mat1rhmcl  22437  dmatmulcl  22456  scmatghm  22489  imacmp  23353  prdstps  23585  symgtgp  24062  prdstgpd  24081  tsmssub  24105  ustuqtop3  24199  utop2nei  24206  xpsxmetlem  24335  xpsmet  24338  imasf1oxms  24445  imasf1oms  24446  prdsmslem1  24483  prdsxmslem1  24484  prdsxmslem2  24485  tngngp2  24608  cnmpopc  24890  caublcls  25277  minveclem3a  25395  efsubm  26528  negleft  28066  negright  28067  noseqrdg0  28315  wlkl1loop  29723  wlkres  29754  clwwlknonex2lem1  30194  eucrct2eupth  30332  subgmulgcld  33137  cyc3co2  33234  sdrgdvcl  33393  sdrginvcl  33394  drgextlsp  33771  fedgmullem2  33808  algextdeglem4  33898  cvmliftlem7  35507  cvmliftlem10  35510  ex-sategoelel  35637  ex-sategoelelomsuc  35642  prdsbnd  38044  prdstotbnd  38045  prdsbnd2  38046  cnpwstotbnd  38048  repwsmet  38085  diblss  41546  kelac1  43420  omcl2  43690  ofoafg  43711  naddwordnexlem0  43753  naddwordnexlem3  43756  iunrelexpuztr  44075  mnuprdlem3  44630  fnchoice  45389  sumnnodd  45990  sublimc  46010  divlimc  46014  cncfshiftioo  46250  itgperiod  46339  stoweidlem26  46384  dirkercncflem2  46462  fourierdlem32  46497  fourierdlem33  46498  fourierdlem46  46510  fourierdlem48  46512  fourierdlem49  46513  fourierdlem62  46526  fourierdlem74  46538  fourierdlem75  46539  fourierdlem76  46540  fourierdlem81  46545  fourierdlem88  46552  fourierdlem89  46553  fourierdlem91  46555  fourierdlem93  46557  fourierdlem103  46567  fourierdlem104  46568  fouriersw  46589  fouriercn  46590  smfco  47160  uspgropssxp  48504  rngccatidALTV  48632  rhmsubcALTVlem3  48643  rhmsubcALTVlem4  48644  ringccatidALTV  48666  srhmsubcALTV  48685  ovmpordxf  48699  discsubc  49423  imaf1co  49514  tposcurf2cl  49661  fuco2eld  49672  fuco22natlem  49704  indthinc  49821  indthincALT  49822  mndtccatid  49946