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 1539   ∈ wcel 2104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728  df-clel 2814

This theorem is referenced by:  elimdelov  7403  ovmpodxf  7455  cantnflt  9474  cantnflem1  9491  cofsmo  10071  cfsmolem  10072  axcclem  10259  smobeth  10388  iccf1o  13274  ccatw2s1p1  14391  ccatw2s1p1OLD  14392  revccat  14524  pwp1fsum  16145  vdwlem8  16734  issubc3  17609  cofucl  17648  catccatid  17866  xpccatid  17950  issstrmgm  18382  mndpropd  18455  issubmnd  18457  pwspjmhm  18513  gsumsgrpccat  18523  gsumccatOLD  18524  smndex1gbas  18586  pwmnd  18621  imasgrp  18736  mulgnndir  18777  subg0cl  18808  subginvcl  18809  subgcl  18810  psgnunilem2  19148  efgsp1  19388  gsumzsubmcl  19564  dpjghm  19711  pwsco1rhm  20027  pwsco2rhm  20028  isdrngd  20061  subrgmcl  20081  subrgunit  20087  issubdrg  20094  lmodprop2d  20230  qsssubdrg  20702  psraddcl  21197  psrmulcllem  21201  psrvscacl  21207  mhppwdeg  21385  matgsum  21631  mat1rhmcl  21675  dmatmulcl  21694  scmatghm  21727  imacmp  22593  prdstps  22825  symgtgp  23302  prdstgpd  23321  tsmssub  23345  ustuqtop3  23440  utop2nei  23447  xpsxmetlem  23577  xpsmet  23580  imasf1oxms  23690  imasf1oms  23691  prdsmslem1  23728  prdsxmslem1  23729  prdsxmslem2  23730  tngngp2  23861  cnmpopc  24136  caublcls  24518  minveclem3a  24636  efsubm  25752  wlkl1loop  28050  wlkres  28083  clwwlknonex2lem1  28516  eucrct2eupth  28654  cyc3co2  31452  drgextlsp  31726  fedgmullem2  31756  cvmliftlem7  33298  cvmliftlem10  33301  ex-sategoelel  33428  ex-sategoelelomsuc  33433  prdsbnd  35995  prdstotbnd  35996  prdsbnd2  35997  cnpwstotbnd  35999  repwsmet  36036  diblss  39226  kelac1  40926  iunrelexpuztr  41365  mnuprdlem3  41930  fnchoice  42610  sumnnodd  43220  sublimc  43242  divlimc  43246  cncfshiftioo  43482  itgperiod  43571  stoweidlem26  43616  dirkercncflem2  43694  fourierdlem32  43729  fourierdlem33  43730  fourierdlem46  43742  fourierdlem48  43744  fourierdlem49  43745  fourierdlem62  43758  fourierdlem74  43770  fourierdlem75  43771  fourierdlem76  43772  fourierdlem81  43777  fourierdlem88  43784  fourierdlem89  43785  fourierdlem91  43787  fourierdlem93  43789  fourierdlem103  43799  fourierdlem104  43800  fouriersw  43821  fouriercn  43822  smfco  44390  uspgropssxp  45364  issubmgm2  45402  rnghmsubcsetclem1  45591  rnghmsubcsetclem2  45592  rngccatidALTV  45605  funcrngcsetc  45614  rhmsubcsetclem1  45637  rhmsubcsetclem2  45638  rhmsubcrngclem1  45643  rhmsubcrngclem2  45644  funcringcsetc  45651  ringccatidALTV  45668  srhmsubc  45692  rhmsubclem3  45704  rhmsubclem4  45705  srhmsubcALTV  45710  rhmsubcALTVlem3  45722  rhmsubcALTVlem4  45723  ovmpordxf  45732  indthinc  46391  indthincALT  46392  mndtccatid  46432