Theorem 3eltr4d 2851

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  elimdelov  7463  ovmpodxf  7517  cantnflt  9593  cantnflem1  9610  cofsmo  10191  cfsmolem  10192  axcclem  10379  smobeth  10509  iccf1o  13449  ccatw2s1p1  14599  revccat  14728  pwp1fsum  16360  vdwlem8  16959  issubc3  17816  cofucl  17855  catccatid  18073  xpccatid  18154  issstrmgm  18621  issubmgm2  18671  sgrppropd  18699  mndpropd  18727  issubmnd  18729  pwspjmhm  18798  gsumsgrpccat  18808  smndex1gbas  18870  smndex1gbasOLD  18871  pwmnd  18908  imasgrp  19032  mulgnndir  19079  subg0cl  19110  subginvcl  19111  subgcl  19112  psgnunilem2  19470  finodsubmsubg  19542  efgsp1  19712  gsumzsubmcl  19893  dpjghm  20040  pwsco1rhm  20479  pwsco2rhm  20480  subrngmcl  20534  subrgunit  20567  rnghmsubcsetclem1  20608  rnghmsubcsetclem2  20609  funcrngcsetc  20617  rhmsubcsetclem1  20637  rhmsubcsetclem2  20638  rhmsubcrngclem1  20643  rhmsubcrngclem2  20644  funcringcsetc  20651  srhmsubc  20657  rhmsubclem3  20664  rhmsubclem4  20665  isdrngd  20742  isdrngdOLD  20744  issubdrg  20757  lmodprop2d  20919  rngqiprngimfo  21299  qsssubdrg  21406  pzriprnglem4  21464  pzriprnglem5  21465  psraddcl  21918  psrmulcllem  21924  psrvscacl  21930  mhppwdeg  22116  psdcl  22127  matgsum  22402  mat1rhmcl  22446  dmatmulcl  22465  scmatghm  22498  imacmp  23362  prdstps  23594  symgtgp  24071  prdstgpd  24090  tsmssub  24114  ustuqtop3  24208  utop2nei  24215  xpsxmetlem  24344  xpsmet  24347  imasf1oxms  24454  imasf1oms  24455  prdsmslem1  24492  prdsxmslem1  24493  prdsxmslem2  24494  tngngp2  24617  cnmpopc  24895  caublcls  25276  minveclem3a  25394  efsubm  26515  negleft  28050  negright  28051  noseqrdg0  28299  wlkl1loop  29706  wlkres  29737  clwwlknonex2lem1  30177  eucrct2eupth  30315  subgmulgcld  33104  cyc3co2  33201  sdrgdvcl  33360  sdrginvcl  33361  drgextlsp  33738  fedgmullem2  33774  algextdeglem4  33864  cvmliftlem7  35473  cvmliftlem10  35476  ex-sategoelel  35603  ex-sategoelelomsuc  35608  prdsbnd  38114  prdstotbnd  38115  prdsbnd2  38116  cnpwstotbnd  38118  repwsmet  38155  diblss  41616  kelac1  43491  omcl2  43761  ofoafg  43782  naddwordnexlem0  43824  naddwordnexlem3  43827  iunrelexpuztr  44146  mnuprdlem3  44701  fnchoice  45460  sumnnodd  46060  sublimc  46080  divlimc  46084  cncfshiftioo  46320  itgperiod  46409  stoweidlem26  46454  dirkercncflem2  46532  fourierdlem32  46567  fourierdlem33  46568  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem62  46596  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem81  46615  fourierdlem88  46622  fourierdlem89  46623  fourierdlem91  46625  fourierdlem93  46627  fourierdlem103  46637  fourierdlem104  46638  fouriersw  46659  fouriercn  46660  smfco  47230  uspgropssxp  48620  rngccatidALTV  48748  rhmsubcALTVlem3  48759  rhmsubcALTVlem4  48760  ringccatidALTV  48782  srhmsubcALTV  48801  ovmpordxf  48815  discsubc  49539  imaf1co  49630  tposcurf2cl  49777  fuco2eld  49788  fuco22natlem  49820  indthinc  49937  indthincALT  49938  mndtccatid  50062