Theorem 3eltr4d 2843

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  elimdelov  7485  ovmpodxf  7539  cantnflt  9625  cantnflem1  9642  cofsmo  10222  cfsmolem  10223  axcclem  10410  smobeth  10539  iccf1o  13457  ccatw2s1p1  14601  revccat  14731  pwp1fsum  16361  vdwlem8  16959  issubc3  17811  cofucl  17850  catccatid  18068  xpccatid  18149  issstrmgm  18580  issubmgm2  18630  sgrppropd  18658  mndpropd  18686  issubmnd  18688  pwspjmhm  18757  gsumsgrpccat  18767  smndex1gbas  18829  pwmnd  18864  imasgrp  18988  mulgnndir  19035  subg0cl  19066  subginvcl  19067  subgcl  19068  psgnunilem2  19425  finodsubmsubg  19497  efgsp1  19667  gsumzsubmcl  19848  dpjghm  19995  pwsco1rhm  20411  pwsco2rhm  20412  subrngmcl  20466  subrgunit  20499  rnghmsubcsetclem1  20540  rnghmsubcsetclem2  20541  funcrngcsetc  20549  rhmsubcsetclem1  20569  rhmsubcsetclem2  20570  rhmsubcrngclem1  20575  rhmsubcrngclem2  20576  funcringcsetc  20583  srhmsubc  20589  rhmsubclem3  20596  rhmsubclem4  20597  isdrngd  20674  isdrngdOLD  20676  issubdrg  20689  lmodprop2d  20830  rngqiprngimfo  21211  qsssubdrg  21343  pzriprnglem4  21394  pzriprnglem5  21395  psraddcl  21847  psraddclOLD  21848  psrmulcllem  21854  psrvscacl  21860  mhppwdeg  22037  psdcl  22048  matgsum  22324  mat1rhmcl  22368  dmatmulcl  22387  scmatghm  22420  imacmp  23284  prdstps  23516  symgtgp  23993  prdstgpd  24012  tsmssub  24036  ustuqtop3  24131  utop2nei  24138  xpsxmetlem  24267  xpsmet  24270  imasf1oxms  24377  imasf1oms  24378  prdsmslem1  24415  prdsxmslem1  24416  prdsxmslem2  24417  tngngp2  24540  cnmpopc  24822  caublcls  25209  minveclem3a  25327  efsubm  26460  noseqrdg0  28201  wlkl1loop  29566  wlkres  29598  clwwlknonex2lem1  30036  eucrct2eupth  30174  subgmulgcld  32984  cyc3co2  33097  sdrgdvcl  33249  sdrginvcl  33250  drgextlsp  33589  fedgmullem2  33626  algextdeglem4  33710  cvmliftlem7  35278  cvmliftlem10  35281  ex-sategoelel  35408  ex-sategoelelomsuc  35413  prdsbnd  37787  prdstotbnd  37788  prdsbnd2  37789  cnpwstotbnd  37791  repwsmet  37828  diblss  41164  kelac1  43052  omcl2  43322  ofoafg  43343  naddwordnexlem0  43385  naddwordnexlem3  43388  iunrelexpuztr  43708  mnuprdlem3  44263  fnchoice  45023  sumnnodd  45628  sublimc  45650  divlimc  45654  cncfshiftioo  45890  itgperiod  45979  stoweidlem26  46024  dirkercncflem2  46102  fourierdlem32  46137  fourierdlem33  46138  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem62  46166  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem81  46185  fourierdlem88  46192  fourierdlem89  46193  fourierdlem91  46195  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  fouriersw  46229  fouriercn  46230  smfco  46800  uspgropssxp  48129  rngccatidALTV  48257  rhmsubcALTVlem3  48268  rhmsubcALTVlem4  48269  ringccatidALTV  48291  srhmsubcALTV  48310  ovmpordxf  48324  discsubc  49050  imaf1co  49141  tposcurf2cl  49288  fuco2eld  49299  fuco22natlem  49331  indthinc  49448  indthincALT  49449  mndtccatid  49573