Theorem 3eltr4d 2844

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722  df-clel 2804

This theorem is referenced by:  elimdelov  7437  ovmpodxf  7491  cantnflt  9557  cantnflem1  9574  cofsmo  10152  cfsmolem  10153  axcclem  10340  smobeth  10469  iccf1o  13388  ccatw2s1p1  14536  revccat  14665  pwp1fsum  16294  vdwlem8  16892  issubc3  17748  cofucl  17787  catccatid  18005  xpccatid  18086  issstrmgm  18553  issubmgm2  18603  sgrppropd  18631  mndpropd  18659  issubmnd  18661  pwspjmhm  18730  gsumsgrpccat  18740  smndex1gbas  18802  pwmnd  18837  imasgrp  18961  mulgnndir  19008  subg0cl  19039  subginvcl  19040  subgcl  19041  psgnunilem2  19400  finodsubmsubg  19472  efgsp1  19642  gsumzsubmcl  19823  dpjghm  19970  pwsco1rhm  20410  pwsco2rhm  20411  subrngmcl  20465  subrgunit  20498  rnghmsubcsetclem1  20539  rnghmsubcsetclem2  20540  funcrngcsetc  20548  rhmsubcsetclem1  20568  rhmsubcsetclem2  20569  rhmsubcrngclem1  20574  rhmsubcrngclem2  20575  funcringcsetc  20582  srhmsubc  20588  rhmsubclem3  20595  rhmsubclem4  20596  isdrngd  20673  isdrngdOLD  20675  issubdrg  20688  lmodprop2d  20850  rngqiprngimfo  21231  qsssubdrg  21356  pzriprnglem4  21414  pzriprnglem5  21415  psraddcl  21868  psraddclOLD  21869  psrmulcllem  21875  psrvscacl  21881  mhppwdeg  22058  psdcl  22069  matgsum  22345  mat1rhmcl  22389  dmatmulcl  22408  scmatghm  22441  imacmp  23305  prdstps  23537  symgtgp  24014  prdstgpd  24033  tsmssub  24057  ustuqtop3  24151  utop2nei  24158  xpsxmetlem  24287  xpsmet  24290  imasf1oxms  24397  imasf1oms  24398  prdsmslem1  24435  prdsxmslem1  24436  prdsxmslem2  24437  tngngp2  24560  cnmpopc  24842  caublcls  25229  minveclem3a  25347  efsubm  26480  noseqrdg0  28230  wlkl1loop  29609  wlkres  29640  clwwlknonex2lem1  30077  eucrct2eupth  30215  subgmulgcld  33014  cyc3co2  33099  sdrgdvcl  33255  sdrginvcl  33256  drgextlsp  33596  fedgmullem2  33633  algextdeglem4  33723  cvmliftlem7  35303  cvmliftlem10  35306  ex-sategoelel  35433  ex-sategoelelomsuc  35438  prdsbnd  37812  prdstotbnd  37813  prdsbnd2  37814  cnpwstotbnd  37816  repwsmet  37853  diblss  41188  kelac1  43075  omcl2  43345  ofoafg  43366  naddwordnexlem0  43408  naddwordnexlem3  43411  iunrelexpuztr  43731  mnuprdlem3  44286  fnchoice  45045  sumnnodd  45649  sublimc  45669  divlimc  45673  cncfshiftioo  45909  itgperiod  45998  stoweidlem26  46043  dirkercncflem2  46121  fourierdlem32  46156  fourierdlem33  46157  fourierdlem46  46169  fourierdlem48  46171  fourierdlem49  46172  fourierdlem62  46185  fourierdlem74  46197  fourierdlem75  46198  fourierdlem76  46199  fourierdlem81  46204  fourierdlem88  46211  fourierdlem89  46212  fourierdlem91  46214  fourierdlem93  46216  fourierdlem103  46226  fourierdlem104  46227  fouriersw  46248  fouriercn  46249  smfco  46819  uspgropssxp  48154  rngccatidALTV  48282  rhmsubcALTVlem3  48293  rhmsubcALTVlem4  48294  ringccatidALTV  48316  srhmsubcALTV  48335  ovmpordxf  48349  discsubc  49075  imaf1co  49166  tposcurf2cl  49313  fuco2eld  49324  fuco22natlem  49356  indthinc  49473  indthincALT  49474  mndtccatid  49598