Theorem 3eltr4d 2847

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

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

This theorem is referenced by:  elimdelov  7508  ovmpodxf  7561  cantnflt  9670  cantnflem1  9687  cofsmo  10267  cfsmolem  10268  axcclem  10455  smobeth  10584  iccf1o  13478  ccatw2s1p1  14591  revccat  14721  pwp1fsum  16339  vdwlem8  16926  issubc3  17804  cofucl  17843  catccatid  18061  xpccatid  18145  issstrmgm  18579  issubmgm2  18629  sgrppropd  18657  mndpropd  18685  issubmnd  18687  pwspjmhm  18748  gsumsgrpccat  18758  smndex1gbas  18820  pwmnd  18855  imasgrp  18976  mulgnndir  19020  subg0cl  19051  subginvcl  19052  subgcl  19053  psgnunilem2  19405  finodsubmsubg  19477  efgsp1  19647  gsumzsubmcl  19828  dpjghm  19975  pwsco1rhm  20394  pwsco2rhm  20395  subrngmcl  20446  subrgunit  20481  isdrngd  20534  isdrngdOLD  20536  issubdrg  20545  lmodprop2d  20679  rngqiprngimfo  21061  qsssubdrg  21205  pzriprnglem4  21254  pzriprnglem5  21255  psraddcl  21722  psrmulcllem  21726  psrvscacl  21732  mhppwdeg  21913  matgsum  22160  mat1rhmcl  22204  dmatmulcl  22223  scmatghm  22256  imacmp  23122  prdstps  23354  symgtgp  23831  prdstgpd  23850  tsmssub  23874  ustuqtop3  23969  utop2nei  23976  xpsxmetlem  24106  xpsmet  24109  imasf1oxms  24219  imasf1oms  24220  prdsmslem1  24257  prdsxmslem1  24258  prdsxmslem2  24259  tngngp2  24390  cnmpopc  24670  caublcls  25058  minveclem3a  25176  efsubm  26297  wlkl1loop  29163  wlkres  29195  clwwlknonex2lem1  29628  eucrct2eupth  29766  cyc3co2  32570  sdrgdvcl  32668  sdrginvcl  32669  drgextlsp  32969  fedgmullem2  33004  algextdeglem4  33066  cvmliftlem7  34581  cvmliftlem10  34584  ex-sategoelel  34711  ex-sategoelelomsuc  34716  prdsbnd  36965  prdstotbnd  36966  prdsbnd2  36967  cnpwstotbnd  36969  repwsmet  37006  diblss  40345  kelac1  42108  omcl2  42386  ofoafg  42407  naddwordnexlem0  42450  naddwordnexlem3  42453  iunrelexpuztr  42773  mnuprdlem3  43336  fnchoice  44016  sumnnodd  44645  sublimc  44667  divlimc  44671  cncfshiftioo  44907  itgperiod  44996  stoweidlem26  45041  dirkercncflem2  45119  fourierdlem32  45154  fourierdlem33  45155  fourierdlem46  45167  fourierdlem48  45169  fourierdlem49  45170  fourierdlem62  45183  fourierdlem74  45195  fourierdlem75  45196  fourierdlem76  45197  fourierdlem81  45202  fourierdlem88  45209  fourierdlem89  45210  fourierdlem91  45212  fourierdlem93  45214  fourierdlem103  45224  fourierdlem104  45225  fouriersw  45246  fouriercn  45247  smfco  45817  uspgropssxp  46821  rnghmsubcsetclem1  46962  rnghmsubcsetclem2  46963  rngccatidALTV  46976  funcrngcsetc  46985  rhmsubcsetclem1  47008  rhmsubcsetclem2  47009  rhmsubcrngclem1  47014  rhmsubcrngclem2  47015  funcringcsetc  47022  ringccatidALTV  47039  srhmsubc  47063  rhmsubclem3  47075  rhmsubclem4  47076  srhmsubcALTV  47081  rhmsubcALTVlem3  47093  rhmsubcALTVlem4  47094  ovmpordxf  47103  indthinc  47760  indthincALT  47761  mndtccatid  47801