Theorem 3eltr4d 2898

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

Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-clel 2863

This theorem is referenced by:  elimdelov  7106  ovmpodxf  7156  cantnflt  8981  cantnflem1  8998  cofsmo  9537  cfsmolem  9538  axcclem  9725  smobeth  9854  iccf1o  12732  ccatw2s1p1  13834  revccat  13964  pwp1fsum  15575  vdwlem8  16153  issubc3  16948  cofucl  16987  catccatid  17191  xpccatid  17267  issstrmgm  17691  mndpropd  17755  issubmnd  17757  pwspjmhm  17807  gsumccat  17817  imasgrp  17972  mulgnndir  18010  subg0cl  18041  subginvcl  18042  subgcl  18043  psgnunilem2  18354  efgsp1  18590  gsumzsubmcl  18758  dpjghm  18902  pwsco1rhm  19180  pwsco2rhm  19181  isdrngd  19217  subrgmcl  19237  subrgunit  19243  issubdrg  19250  lmodprop2d  19386  psraddcl  19851  psrmulcllem  19855  psrvscacl  19861  qsssubdrg  20286  matgsum  20730  mat1rhmcl  20774  dmatmulcl  20793  scmatghm  20826  imacmp  21689  prdstps  21921  symgtgp  22393  prdstgpd  22416  tsmssub  22440  ustuqtop3  22535  utop2nei  22542  xpsxmetlem  22672  xpsmet  22675  imasf1oxms  22782  imasf1oms  22783  prdsmslem1  22820  prdsxmslem1  22821  prdsxmslem2  22822  tngngp2  22944  cnmpopc  23215  caublcls  23595  minveclem3a  23713  efsubm  24816  wlkl1loop  27102  wlkres  27135  clwwlknonex2lem1  27573  eucrct2eupthOLD  27713  eucrct2eupth  27714  cyc3co2  30419  drgextlsp  30600  fedgmullem2  30630  cvmliftlem7  32146  cvmliftlem10  32149  ex-sategoelel  32276  ex-sategoelelomsuc  32281  prdsbnd  34603  prdstotbnd  34604  prdsbnd2  34605  cnpwstotbnd  34607  repwsmet  34644  diblss  37837  kelac1  39148  iunrelexpuztr  39549  mnuprdlem3  40107  fnchoice  40825  sumnnodd  41453  sublimc  41475  divlimc  41479  cncfshiftioo  41716  itgperiod  41807  stoweidlem26  41853  dirkercncflem2  41931  fourierdlem32  41966  fourierdlem33  41967  fourierdlem46  41979  fourierdlem48  41981  fourierdlem49  41982  fourierdlem62  41995  fourierdlem74  42007  fourierdlem75  42008  fourierdlem76  42009  fourierdlem81  42014  fourierdlem88  42021  fourierdlem89  42022  fourierdlem91  42024  fourierdlem93  42026  fourierdlem103  42036  fourierdlem104  42037  fouriersw  42058  fouriercn  42059  uspgropssxp  43501  issubmgm2  43539  rnghmsubcsetclem1  43724  rnghmsubcsetclem2  43725  rngccatidALTV  43738  funcrngcsetc  43747  rhmsubcsetclem1  43770  rhmsubcsetclem2  43771  rhmsubcrngclem1  43776  rhmsubcrngclem2  43777  funcringcsetc  43784  ringccatidALTV  43801  srhmsubc  43825  rhmsubclem3  43837  rhmsubclem4  43838  srhmsubcALTV  43843  rhmsubcALTVlem3  43855  rhmsubcALTVlem4  43856  ovmpordxf  43865