Theorem 3eltr4d 2848

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  elimdelov  7507  ovmpodxf  7560  cantnflt  9669  cantnflem1  9686  cofsmo  10266  cfsmolem  10267  axcclem  10454  smobeth  10583  iccf1o  13475  ccatw2s1p1  14588  revccat  14718  pwp1fsum  16336  vdwlem8  16923  issubc3  17801  cofucl  17840  catccatid  18058  xpccatid  18142  issstrmgm  18574  sgrppropd  18624  mndpropd  18652  issubmnd  18654  pwspjmhm  18713  gsumsgrpccat  18723  smndex1gbas  18785  pwmnd  18820  imasgrp  18941  mulgnndir  18985  subg0cl  19016  subginvcl  19017  subgcl  19018  psgnunilem2  19365  finodsubmsubg  19437  efgsp1  19607  gsumzsubmcl  19788  dpjghm  19935  pwsco1rhm  20281  pwsco2rhm  20282  subrgmcl  20335  subrgunit  20341  isdrngd  20394  isdrngdOLD  20396  issubdrg  20405  lmodprop2d  20539  qsssubdrg  21010  psraddcl  21508  psrmulcllem  21512  psrvscacl  21518  mhppwdeg  21699  matgsum  21946  mat1rhmcl  21990  dmatmulcl  22009  scmatghm  22042  imacmp  22908  prdstps  23140  symgtgp  23617  prdstgpd  23636  tsmssub  23660  ustuqtop3  23755  utop2nei  23762  xpsxmetlem  23892  xpsmet  23895  imasf1oxms  24005  imasf1oms  24006  prdsmslem1  24043  prdsxmslem1  24044  prdsxmslem2  24045  tngngp2  24176  cnmpopc  24451  caublcls  24833  minveclem3a  24951  efsubm  26067  wlkl1loop  28933  wlkres  28965  clwwlknonex2lem1  29398  eucrct2eupth  29536  cyc3co2  32340  sdrgdvcl  32438  sdrginvcl  32439  drgextlsp  32739  fedgmullem2  32774  algextdeglem4  32836  cvmliftlem7  34351  cvmliftlem10  34354  ex-sategoelel  34481  ex-sategoelelomsuc  34486  prdsbnd  36747  prdstotbnd  36748  prdsbnd2  36749  cnpwstotbnd  36751  repwsmet  36788  diblss  40127  kelac1  41887  omcl2  42165  ofoafg  42186  naddwordnexlem0  42229  naddwordnexlem3  42232  iunrelexpuztr  42552  mnuprdlem3  43115  fnchoice  43795  sumnnodd  44425  sublimc  44447  divlimc  44451  cncfshiftioo  44687  itgperiod  44776  stoweidlem26  44821  dirkercncflem2  44899  fourierdlem32  44934  fourierdlem33  44935  fourierdlem46  44947  fourierdlem48  44949  fourierdlem49  44950  fourierdlem62  44963  fourierdlem74  44975  fourierdlem75  44976  fourierdlem76  44977  fourierdlem81  44982  fourierdlem88  44989  fourierdlem89  44990  fourierdlem91  44992  fourierdlem93  44994  fourierdlem103  45004  fourierdlem104  45005  fouriersw  45026  fouriercn  45027  smfco  45597  uspgropssxp  46601  issubmgm2  46639  subrngmcl  46815  rngqiprngimfo  46865  pzriprnglem4  46887  pzriprnglem5  46888  rnghmsubcsetclem1  46952  rnghmsubcsetclem2  46953  rngccatidALTV  46966  funcrngcsetc  46975  rhmsubcsetclem1  46998  rhmsubcsetclem2  46999  rhmsubcrngclem1  47004  rhmsubcrngclem2  47005  funcringcsetc  47012  ringccatidALTV  47029  srhmsubc  47053  rhmsubclem3  47065  rhmsubclem4  47066  srhmsubcALTV  47071  rhmsubcALTVlem3  47083  rhmsubcALTVlem4  47084  ovmpordxf  47093  indthinc  47750  indthincALT  47751  mndtccatid  47791