Theorem 3eltr4d 2849

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809

This theorem is referenced by:  elimdelov  7452  ovmpodxf  7506  cantnflt  9579  cantnflem1  9596  cofsmo  10177  cfsmolem  10178  axcclem  10365  smobeth  10495  iccf1o  13410  ccatw2s1p1  14558  revccat  14687  pwp1fsum  16316  vdwlem8  16914  issubc3  17771  cofucl  17810  catccatid  18028  xpccatid  18109  issstrmgm  18576  issubmgm2  18626  sgrppropd  18654  mndpropd  18682  issubmnd  18684  pwspjmhm  18753  gsumsgrpccat  18763  smndex1gbas  18825  pwmnd  18860  imasgrp  18984  mulgnndir  19031  subg0cl  19062  subginvcl  19063  subgcl  19064  psgnunilem2  19422  finodsubmsubg  19494  efgsp1  19664  gsumzsubmcl  19845  dpjghm  19992  pwsco1rhm  20433  pwsco2rhm  20434  subrngmcl  20488  subrgunit  20521  rnghmsubcsetclem1  20562  rnghmsubcsetclem2  20563  funcrngcsetc  20571  rhmsubcsetclem1  20591  rhmsubcsetclem2  20592  rhmsubcrngclem1  20597  rhmsubcrngclem2  20598  funcringcsetc  20605  srhmsubc  20611  rhmsubclem3  20618  rhmsubclem4  20619  isdrngd  20696  isdrngdOLD  20698  issubdrg  20711  lmodprop2d  20873  rngqiprngimfo  21254  qsssubdrg  21379  pzriprnglem4  21437  pzriprnglem5  21438  psraddcl  21892  psraddclOLD  21893  psrmulcllem  21899  psrvscacl  21905  mhppwdeg  22091  psdcl  22102  matgsum  22379  mat1rhmcl  22423  dmatmulcl  22442  scmatghm  22475  imacmp  23339  prdstps  23571  symgtgp  24048  prdstgpd  24067  tsmssub  24091  ustuqtop3  24185  utop2nei  24192  xpsxmetlem  24321  xpsmet  24324  imasf1oxms  24431  imasf1oms  24432  prdsmslem1  24469  prdsxmslem1  24470  prdsxmslem2  24471  tngngp2  24594  cnmpopc  24876  caublcls  25263  minveclem3a  25381  efsubm  26514  negsleft  28027  negsright  28028  noseqrdg0  28268  wlkl1loop  29660  wlkres  29691  clwwlknonex2lem1  30131  eucrct2eupth  30269  subgmulgcld  33075  cyc3co2  33171  sdrgdvcl  33330  sdrginvcl  33331  drgextlsp  33699  fedgmullem2  33736  algextdeglem4  33826  cvmliftlem7  35434  cvmliftlem10  35437  ex-sategoelel  35564  ex-sategoelelomsuc  35569  prdsbnd  37933  prdstotbnd  37934  prdsbnd2  37935  cnpwstotbnd  37937  repwsmet  37974  diblss  41369  kelac1  43247  omcl2  43517  ofoafg  43538  naddwordnexlem0  43580  naddwordnexlem3  43583  iunrelexpuztr  43902  mnuprdlem3  44457  fnchoice  45216  sumnnodd  45818  sublimc  45838  divlimc  45842  cncfshiftioo  46078  itgperiod  46167  stoweidlem26  46212  dirkercncflem2  46290  fourierdlem32  46325  fourierdlem33  46326  fourierdlem46  46338  fourierdlem48  46340  fourierdlem49  46341  fourierdlem62  46354  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem81  46373  fourierdlem88  46380  fourierdlem89  46381  fourierdlem91  46383  fourierdlem93  46385  fourierdlem103  46395  fourierdlem104  46396  fouriersw  46417  fouriercn  46418  smfco  46988  uspgropssxp  48332  rngccatidALTV  48460  rhmsubcALTVlem3  48471  rhmsubcALTVlem4  48472  ringccatidALTV  48494  srhmsubcALTV  48513  ovmpordxf  48527  discsubc  49251  imaf1co  49342  tposcurf2cl  49489  fuco2eld  49500  fuco22natlem  49532  indthinc  49649  indthincALT  49650  mndtccatid  49774