Theorem 3eltr4d 2875

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  elimdelov  7510  ovmpodxf  7564  cantnflt  9652  cantnflem1  9669  cofsmo  10272  cfsmolem  10273  axcclem  10460  smobeth  10596  iccf1o  13550  ccatw2s1p1  14705  revccat  14836  pwp1fsum  16482  vdwlem8  17081  issubc3  17939  cofucl  17978  catccatid  18196  xpccatid  18277  issstrmgm  18746  issubmgm2  18806  sgrppropd  18834  mndpropd  18865  issubmnd  18867  pwspjmhm  18940  gsumsgrpccat  18950  smndex1gbas  19012  smndex1gbasOLD  19013  pwmnd  19057  imasgrp  19180  mulgnndir  19227  subg0cl  19258  subginvcl  19259  subgcl  19260  psgnunilem2  19623  finodsubmsubg  19695  efgsp1  19865  gsumzsubmcl  20046  dpjghm  20193  pwsco1rhm  20653  pwsco2rhm  20654  subrngmcl  20720  subrgunit  20753  rnghmsubcsetclem1  20794  rnghmsubcsetclem2  20795  funcrngcsetc  20803  rhmsubcsetclem1  20823  rhmsubcsetclem2  20824  rhmsubcrngclem1  20829  rhmsubcrngclem2  20830  funcringcsetc  20837  srhmsubc  20843  rhmsubclem3  20850  rhmsubclem4  20851  isdrngd  20932  isdrngdOLD  20934  issubdrg  20947  lmodprop2d  21109  rngqiprngimfo  21505  qsssubdrg  21640  pzriprnglem4  21698  pzriprnglem5  21699  psraddcl  22155  psrmulcllem  22161  psrvscacl  22167  mhppwdeg  22379  psdcl  22390  matgsum  22660  mat1rhmcl  22704  dmatmulcl  22723  scmatghm  22756  imacmp  23623  prdstps  23856  symgtgp  24333  prdstgpd  24352  tsmssub  24376  ustuqtop3  24470  utop2nei  24477  xpsxmetlem  24606  xpsmet  24609  imasf1oxms  24716  imasf1oms  24717  prdsmslem1  24754  prdsxmslem1  24755  prdsxmslem2  24756  tngngp2  24879  cnmpopc  25157  caublcls  25538  minveclem3a  25656  efsubm  26789  negleft  28324  negright  28325  noseqrdg0  28573  angmgmaddov2  29269  wlkl1loop  30098  wlkres  30129  clwwlknonex2lem1  30578  eucrct2eupth  30726  subgmulgcld  33484  cyc3co2  33581  sdrgdvcl  33741  sdrginvcl  33742  drgextlsp  34105  fedgmullem2  34141  algextdeglem4  34231  cvmliftlem7  35871  cvmliftlem10  35874  ex-sategoelel  36001  ex-sategoelelomsuc  36006  nadddilem1  36801  nadddilem2  36802  nadddilem3  36803  nadddilem4  36804  prdsbnd  38544  prdstotbnd  38545  prdsbnd2  38546  cnpwstotbnd  38548  repwsmet  38585  diblss  42044  kelac1  43905  omcl2  44175  ofoafg  44196  naddwordnexlem0  44238  naddwordnexlem3  44241  iunrelexpuztr  44560  mnuprdlem3  45099  fnchoice  45864  sumnnodd  46461  sublimc  46481  divlimc  46485  cncfshiftioo  46721  itgperiod  46810  stoweidlem26  46855  dirkercncflem2  46933  fourierdlem32  46968  fourierdlem33  46969  fourierdlem46  46981  fourierdlem48  46983  fourierdlem49  46984  fourierdlem62  46997  fourierdlem74  47009  fourierdlem75  47010  fourierdlem76  47011  fourierdlem81  47016  fourierdlem88  47023  fourierdlem89  47024  fourierdlem91  47026  fourierdlem93  47028  fourierdlem103  47038  fourierdlem104  47039  fouriersw  47060  fouriercn  47061  smfco  47631  uspgropssxp  49061  rngccatidALTV  49188  rhmsubcALTVlem3  49199  rhmsubcALTVlem4  49200  ringccatidALTV  49222  srhmsubcALTV  49241  ovmpordxf  49270  discsubc  49991  imaf1co  50082  tposcurf2cl  50229  fuco2eld  50240  fuco22natlem  50272  indthinc  50389  indthincALT  50390  mndtccatid  50514