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  7445  ovmpodxf  7499  cantnflt  9568  cantnflem1  9585  cofsmo  10163  cfsmolem  10164  axcclem  10351  smobeth  10480  iccf1o  13399  ccatw2s1p1  14543  revccat  14672  pwp1fsum  16302  vdwlem8  16900  issubc3  17756  cofucl  17795  catccatid  18013  xpccatid  18094  issstrmgm  18527  issubmgm2  18577  sgrppropd  18605  mndpropd  18633  issubmnd  18635  pwspjmhm  18704  gsumsgrpccat  18714  smndex1gbas  18776  pwmnd  18811  imasgrp  18935  mulgnndir  18982  subg0cl  19013  subginvcl  19014  subgcl  19015  psgnunilem2  19374  finodsubmsubg  19446  efgsp1  19616  gsumzsubmcl  19797  dpjghm  19944  pwsco1rhm  20387  pwsco2rhm  20388  subrngmcl  20442  subrgunit  20475  rnghmsubcsetclem1  20516  rnghmsubcsetclem2  20517  funcrngcsetc  20525  rhmsubcsetclem1  20545  rhmsubcsetclem2  20546  rhmsubcrngclem1  20551  rhmsubcrngclem2  20552  funcringcsetc  20559  srhmsubc  20565  rhmsubclem3  20572  rhmsubclem4  20573  isdrngd  20650  isdrngdOLD  20652  issubdrg  20665  lmodprop2d  20827  rngqiprngimfo  21208  qsssubdrg  21333  pzriprnglem4  21391  pzriprnglem5  21392  psraddcl  21845  psraddclOLD  21846  psrmulcllem  21852  psrvscacl  21858  mhppwdeg  22035  psdcl  22046  matgsum  22322  mat1rhmcl  22366  dmatmulcl  22385  scmatghm  22418  imacmp  23282  prdstps  23514  symgtgp  23991  prdstgpd  24010  tsmssub  24034  ustuqtop3  24129  utop2nei  24136  xpsxmetlem  24265  xpsmet  24268  imasf1oxms  24375  imasf1oms  24376  prdsmslem1  24413  prdsxmslem1  24414  prdsxmslem2  24415  tngngp2  24538  cnmpopc  24820  caublcls  25207  minveclem3a  25325  efsubm  26458  noseqrdg0  28206  wlkl1loop  29583  wlkres  29614  clwwlknonex2lem1  30051  eucrct2eupth  30189  subgmulgcld  32997  cyc3co2  33082  sdrgdvcl  33238  sdrginvcl  33239  drgextlsp  33560  fedgmullem2  33597  algextdeglem4  33687  cvmliftlem7  35268  cvmliftlem10  35271  ex-sategoelel  35398  ex-sategoelelomsuc  35403  prdsbnd  37777  prdstotbnd  37778  prdsbnd2  37779  cnpwstotbnd  37781  repwsmet  37818  diblss  41153  kelac1  43040  omcl2  43310  ofoafg  43331  naddwordnexlem0  43373  naddwordnexlem3  43376  iunrelexpuztr  43696  mnuprdlem3  44251  fnchoice  45011  sumnnodd  45615  sublimc  45637  divlimc  45641  cncfshiftioo  45877  itgperiod  45966  stoweidlem26  46011  dirkercncflem2  46089  fourierdlem32  46124  fourierdlem33  46125  fourierdlem46  46137  fourierdlem48  46139  fourierdlem49  46140  fourierdlem62  46153  fourierdlem74  46165  fourierdlem75  46166  fourierdlem76  46167  fourierdlem81  46172  fourierdlem88  46179  fourierdlem89  46180  fourierdlem91  46182  fourierdlem93  46184  fourierdlem103  46194  fourierdlem104  46195  fouriersw  46216  fouriercn  46217  smfco  46787  uspgropssxp  48132  rngccatidALTV  48260  rhmsubcALTVlem3  48271  rhmsubcALTVlem4  48272  ringccatidALTV  48294  srhmsubcALTV  48313  ovmpordxf  48327  discsubc  49053  imaf1co  49144  tposcurf2cl  49291  fuco2eld  49302  fuco22natlem  49334  indthinc  49451  indthincALT  49452  mndtccatid  49576