Theorem 3eltr4d 2884

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  elimdelov  7507  ovmpodxf  7561  cantnflt  9641  cantnflem1  9658  cofsmo  10253  cfsmolem  10254  axcclem  10441  smobeth  10571  iccf1o  13523  ccatw2s1p1  14674  revccat  14803  pwp1fsum  16449  vdwlem8  17048  issubc3  17906  cofucl  17945  catccatid  18163  xpccatid  18244  issstrmgm  18711  issubmgm2  18761  sgrppropd  18789  mndpropd  18817  issubmnd  18819  pwspjmhm  18889  gsumsgrpccat  18899  smndex1gbas  18961  smndex1gbasOLD  18962  pwmnd  18999  imasgrp  19122  mulgnndir  19169  subg0cl  19200  subginvcl  19201  subgcl  19202  psgnunilem2  19565  finodsubmsubg  19637  efgsp1  19807  gsumzsubmcl  19988  dpjghm  20135  pwsco1rhm  20584  pwsco2rhm  20585  subrngmcl  20642  subrgunit  20675  rnghmsubcsetclem1  20716  rnghmsubcsetclem2  20717  funcrngcsetc  20725  rhmsubcsetclem1  20745  rhmsubcsetclem2  20746  rhmsubcrngclem1  20751  rhmsubcrngclem2  20752  funcringcsetc  20759  srhmsubc  20765  rhmsubclem3  20772  rhmsubclem4  20773  isdrngd  20847  isdrngdOLD  20849  issubdrg  20861  lmodprop2d  21023  rngqiprngimfo  21412  qsssubdrg  21545  pzriprnglem4  21603  pzriprnglem5  21604  psraddcl  22058  psrmulcllem  22064  psrvscacl  22070  mhppwdeg  22282  psdcl  22293  matgsum  22563  mat1rhmcl  22607  dmatmulcl  22626  scmatghm  22659  imacmp  23523  prdstps  23755  symgtgp  24232  prdstgpd  24251  tsmssub  24275  ustuqtop3  24369  utop2nei  24376  xpsxmetlem  24505  xpsmet  24508  imasf1oxms  24615  imasf1oms  24616  prdsmslem1  24653  prdsxmslem1  24654  prdsxmslem2  24655  tngngp2  24778  cnmpopc  25056  caublcls  25437  minveclem3a  25555  efsubm  26682  negleft  28217  negright  28218  noseqrdg0  28466  wlkl1loop  29928  wlkres  29959  clwwlknonex2lem1  30399  eucrct2eupth  30537  subgmulgcld  33304  cyc3co2  33401  sdrgdvcl  33563  sdrginvcl  33564  drgextlsp  33929  fedgmullem2  33965  algextdeglem4  34055  cvmliftlem7  35682  cvmliftlem10  35685  ex-sategoelel  35812  ex-sategoelelomsuc  35817  prdsbnd  38332  prdstotbnd  38333  prdsbnd2  38334  cnpwstotbnd  38336  repwsmet  38373  diblss  41834  kelac1  43682  omcl2  43952  ofoafg  43973  naddwordnexlem0  44015  naddwordnexlem3  44018  iunrelexpuztr  44337  mnuprdlem3  44876  fnchoice  45641  sumnnodd  46238  sublimc  46258  divlimc  46262  cncfshiftioo  46498  itgperiod  46587  stoweidlem26  46632  dirkercncflem2  46710  fourierdlem32  46745  fourierdlem33  46746  fourierdlem46  46758  fourierdlem48  46760  fourierdlem49  46761  fourierdlem62  46774  fourierdlem74  46786  fourierdlem75  46787  fourierdlem76  46788  fourierdlem81  46793  fourierdlem88  46800  fourierdlem89  46801  fourierdlem91  46803  fourierdlem93  46805  fourierdlem103  46815  fourierdlem104  46816  fouriersw  46837  fouriercn  46838  smfco  47408  uspgropssxp  48798  rngccatidALTV  48926  rhmsubcALTVlem3  48937  rhmsubcALTVlem4  48938  ringccatidALTV  48960  srhmsubcALTV  48979  ovmpordxf  49004  discsubc  49727  imaf1co  49818  tposcurf2cl  49965  fuco2eld  49976  fuco22natlem  50008  indthinc  50125  indthincALT  50126  mndtccatid  50250