Theorem 3eltr4d 2928

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  elimdelov  7250  ovmpodxf  7300  cantnflt  9135  cantnflem1  9152  cofsmo  9691  cfsmolem  9692  axcclem  9879  smobeth  10008  iccf1o  12883  ccatw2s1p1  13995  ccatw2s1p1OLD  13996  revccat  14128  pwp1fsum  15742  vdwlem8  16324  issubc3  17119  cofucl  17158  catccatid  17362  xpccatid  17438  issstrmgm  17863  mndpropd  17936  issubmnd  17938  pwspjmhm  17994  gsumsgrpccat  18004  gsumccatOLD  18005  smndex1gbas  18067  pwmnd  18102  imasgrp  18215  mulgnndir  18256  subg0cl  18287  subginvcl  18288  subgcl  18289  psgnunilem2  18623  efgsp1  18863  gsumzsubmcl  19038  dpjghm  19185  pwsco1rhm  19490  pwsco2rhm  19491  isdrngd  19527  subrgmcl  19547  subrgunit  19553  issubdrg  19560  lmodprop2d  19696  psraddcl  20163  psrmulcllem  20167  psrvscacl  20173  qsssubdrg  20604  matgsum  21046  mat1rhmcl  21090  dmatmulcl  21109  scmatghm  21142  imacmp  22005  prdstps  22237  symgtgp  22714  prdstgpd  22733  tsmssub  22757  ustuqtop3  22852  utop2nei  22859  xpsxmetlem  22989  xpsmet  22992  imasf1oxms  23099  imasf1oms  23100  prdsmslem1  23137  prdsxmslem1  23138  prdsxmslem2  23139  tngngp2  23261  cnmpopc  23532  caublcls  23912  minveclem3a  24030  efsubm  25135  wlkl1loop  27419  wlkres  27452  clwwlknonex2lem1  27886  eucrct2eupth  28024  cyc3co2  30782  drgextlsp  30996  fedgmullem2  31026  cvmliftlem7  32538  cvmliftlem10  32541  ex-sategoelel  32668  ex-sategoelelomsuc  32673  prdsbnd  35086  prdstotbnd  35087  prdsbnd2  35088  cnpwstotbnd  35090  repwsmet  35127  diblss  38321  kelac1  39712  iunrelexpuztr  40113  mnuprdlem3  40659  fnchoice  41335  sumnnodd  41960  sublimc  41982  divlimc  41986  cncfshiftioo  42224  itgperiod  42315  stoweidlem26  42360  dirkercncflem2  42438  fourierdlem32  42473  fourierdlem33  42474  fourierdlem46  42486  fourierdlem48  42488  fourierdlem49  42489  fourierdlem62  42502  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem81  42521  fourierdlem88  42528  fourierdlem89  42529  fourierdlem91  42531  fourierdlem93  42533  fourierdlem103  42543  fourierdlem104  42544  fouriersw  42565  fouriercn  42566  uspgropssxp  44068  issubmgm2  44106  rnghmsubcsetclem1  44295  rnghmsubcsetclem2  44296  rngccatidALTV  44309  funcrngcsetc  44318  rhmsubcsetclem1  44341  rhmsubcsetclem2  44342  rhmsubcrngclem1  44347  rhmsubcrngclem2  44348  funcringcsetc  44355  ringccatidALTV  44372  srhmsubc  44396  rhmsubclem3  44408  rhmsubclem4  44409  srhmsubcALTV  44414  rhmsubcALTVlem3  44426  rhmsubcALTVlem4  44427  ovmpordxf  44436