Theorem 3eltr4d 2852

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  elimdelov  7457  ovmpodxf  7511  cantnflt  9587  cantnflem1  9604  cofsmo  10185  cfsmolem  10186  axcclem  10373  smobeth  10503  iccf1o  13443  ccatw2s1p1  14593  revccat  14722  pwp1fsum  16354  vdwlem8  16953  issubc3  17810  cofucl  17849  catccatid  18067  xpccatid  18148  issstrmgm  18615  issubmgm2  18665  sgrppropd  18693  mndpropd  18721  issubmnd  18723  pwspjmhm  18792  gsumsgrpccat  18802  smndex1gbas  18864  smndex1gbasOLD  18865  pwmnd  18902  imasgrp  19026  mulgnndir  19073  subg0cl  19104  subginvcl  19105  subgcl  19106  psgnunilem2  19464  finodsubmsubg  19536  efgsp1  19706  gsumzsubmcl  19887  dpjghm  20034  pwsco1rhm  20473  pwsco2rhm  20474  subrngmcl  20528  subrgunit  20561  rnghmsubcsetclem1  20602  rnghmsubcsetclem2  20603  funcrngcsetc  20611  rhmsubcsetclem1  20631  rhmsubcsetclem2  20632  rhmsubcrngclem1  20637  rhmsubcrngclem2  20638  funcringcsetc  20645  srhmsubc  20651  rhmsubclem3  20658  rhmsubclem4  20659  isdrngd  20736  isdrngdOLD  20738  issubdrg  20751  lmodprop2d  20913  rngqiprngimfo  21294  qsssubdrg  21419  pzriprnglem4  21477  pzriprnglem5  21478  psraddcl  21931  psrmulcllem  21937  psrvscacl  21943  mhppwdeg  22129  psdcl  22140  matgsum  22415  mat1rhmcl  22459  dmatmulcl  22478  scmatghm  22511  imacmp  23375  prdstps  23607  symgtgp  24084  prdstgpd  24103  tsmssub  24127  ustuqtop3  24221  utop2nei  24228  xpsxmetlem  24357  xpsmet  24360  imasf1oxms  24467  imasf1oms  24468  prdsmslem1  24505  prdsxmslem1  24506  prdsxmslem2  24507  tngngp2  24630  cnmpopc  24908  caublcls  25289  minveclem3a  25407  efsubm  26531  negleft  28067  negright  28068  noseqrdg0  28316  wlkl1loop  29724  wlkres  29755  clwwlknonex2lem1  30195  eucrct2eupth  30333  subgmulgcld  33122  cyc3co2  33219  sdrgdvcl  33378  sdrginvcl  33379  drgextlsp  33756  fedgmullem2  33793  algextdeglem4  33883  cvmliftlem7  35492  cvmliftlem10  35495  ex-sategoelel  35622  ex-sategoelelomsuc  35627  prdsbnd  38131  prdstotbnd  38132  prdsbnd2  38133  cnpwstotbnd  38135  repwsmet  38172  diblss  41633  kelac1  43512  omcl2  43782  ofoafg  43803  naddwordnexlem0  43845  naddwordnexlem3  43848  iunrelexpuztr  44167  mnuprdlem3  44722  fnchoice  45481  sumnnodd  46081  sublimc  46101  divlimc  46105  cncfshiftioo  46341  itgperiod  46430  stoweidlem26  46475  dirkercncflem2  46553  fourierdlem32  46588  fourierdlem33  46589  fourierdlem46  46601  fourierdlem48  46603  fourierdlem49  46604  fourierdlem62  46617  fourierdlem74  46629  fourierdlem75  46630  fourierdlem76  46631  fourierdlem81  46636  fourierdlem88  46643  fourierdlem89  46644  fourierdlem91  46646  fourierdlem93  46648  fourierdlem103  46658  fourierdlem104  46659  fouriersw  46680  fouriercn  46681  smfco  47251  uspgropssxp  48635  rngccatidALTV  48763  rhmsubcALTVlem3  48774  rhmsubcALTVlem4  48775  ringccatidALTV  48797  srhmsubcALTV  48816  ovmpordxf  48830  discsubc  49554  imaf1co  49645  tposcurf2cl  49792  fuco2eld  49803  fuco22natlem  49835  indthinc  49952  indthincALT  49953  mndtccatid  50077