Theorem 3eltr4d 2879

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  elimdelov  7547  ovmpodxf  7602  cantnflt  9710  cantnflem1  9727  cofsmo  10386  cfsmolem  10387  axcclem  10574  smobeth  10710  iccf1o  13667  ccatw2s1p1  14826  revccat  14957  pwp1fsum  16605  vdwlem8  17210  issubc3  18074  cofucl  18113  catccatid  18331  xpccatid  18412  issstrmgm  18881  issubmgm2  18942  sgrppropd  18970  mndpropd  19001  issubmnd  19003  pwspjmhm  19076  gsumsgrpccat  19086  smndex1gbas  19148  smndex1gbasOLD  19149  pwmnd  19193  imasgrp  19316  mulgnndir  19363  subg0cl  19394  subginvcl  19395  subgcl  19396  psgnunilem2  19760  finodsubmsubg  19832  efgsp1  20002  gsumzsubmcl  20183  dpjghm  20330  pwsco1rhm  20792  pwsco2rhm  20793  subrngmcl  20860  subrgunit  20893  rnghmsubcsetclem1  20934  rnghmsubcsetclem2  20935  funcrngcsetc  20943  rhmsubcsetclem1  20963  rhmsubcsetclem2  20964  rhmsubcrngclem1  20969  rhmsubcrngclem2  20970  funcringcsetc  20977  srhmsubc  20983  rhmsubclem3  20990  rhmsubclem4  20991  isdrngd  21073  isdrngdOLD  21075  issubdrg  21088  lmodprop2d  21250  rngqiprngimfo  21648  qsssubdrg  21786  pzriprnglem4  21845  pzriprnglem5  21846  psraddcl  22302  psrmulcllem  22308  psrvscacl  22314  mhppwdeg  22526  psdcl  22537  matgsum  22807  mat1rhmcl  22851  dmatmulcl  22870  scmatghm  22903  imacmp  23770  prdstps  24003  symgtgp  24480  prdstgpd  24499  tsmssub  24523  ustuqtop3  24617  utop2nei  24624  xpsxmetlem  24753  xpsmet  24756  imasf1oxms  24863  imasf1oms  24864  prdsmslem1  24901  prdsxmslem1  24902  prdsxmslem2  24903  tngngp2  25026  cnmpopc  25304  caublcls  25685  minveclem3a  25803  efsubm  26936  negleft  28501  negright  28502  noseqrdg0  28750  angmgmaddov2  29446  wlkl1loop  30275  wlkres  30306  clwwlknonex2lem1  30755  eucrct2eupth  30903  subgmulgcld  33703  cyc3co2  33800  sdrgdvcl  33965  sdrginvcl  33966  drgextlsp  34337  fedgmullem2  34373  algextdeglem4  34463  cvmliftlem7  36264  cvmliftlem10  36267  ex-sategoelel  36394  ex-sategoelelomsuc  36399  nadddilem1  37184  nadddilem2  37185  nadddilem3  37186  nadddilem4  37187  prdsbnd  38993  prdstotbnd  38994  prdsbnd2  38995  cnpwstotbnd  38997  repwsmet  39034  diblss  42493  kelac1  44331  omcl2  44596  ofoafg  44617  naddwordnexlem0  44659  naddwordnexlem3  44662  iunrelexpuztr  44980  mnuprdlem3  45519  fnchoice  46320  sumnnodd  46915  sublimc  46935  divlimc  46939  cncfshiftioo  47175  itgperiod  47264  stoweidlem26  47309  dirkercncflem2  47387  fourierdlem32  47422  fourierdlem33  47423  fourierdlem46  47435  fourierdlem48  47437  fourierdlem49  47438  fourierdlem62  47451  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem81  47470  fourierdlem88  47477  fourierdlem89  47478  fourierdlem91  47480  fourierdlem93  47482  fourierdlem103  47492  fourierdlem104  47493  fouriersw  47514  fouriercn  47515  smfco  48085  uspgropssxp  49515  rngccatidALTV  49642  rhmsubcALTVlem3  49653  rhmsubcALTVlem4  49654  ringccatidALTV  49676  srhmsubcALTV  49695  lazmulzcl  49737  lazaddcl  49738  ovmpordxf  49782  discsubc  50509  imaf1co  50602  tposcurf2cl  50755  fuco2eld  50766  fuco22natlem  50798  indthinc  50928  indthincALT  50929  mndtccatid  51056  parhomco2  51091  parhomco  51092