Theorem 3eltr4d 2847

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809

This theorem is referenced by:  elimdelov  7458  ovmpodxf  7510  cantnflt  9617  cantnflem1  9634  cofsmo  10214  cfsmolem  10215  axcclem  10402  smobeth  10531  iccf1o  13423  ccatw2s1p1  14536  revccat  14666  pwp1fsum  16284  vdwlem8  16871  issubc3  17749  cofucl  17788  catccatid  18006  xpccatid  18090  issstrmgm  18522  mndpropd  18595  issubmnd  18597  pwspjmhm  18654  gsumsgrpccat  18664  smndex1gbas  18726  pwmnd  18761  imasgrp  18877  mulgnndir  18919  subg0cl  18950  subginvcl  18951  subgcl  18952  psgnunilem2  19291  finodsubmsubg  19363  efgsp1  19533  gsumzsubmcl  19709  dpjghm  19856  pwsco1rhm  20188  pwsco2rhm  20189  isdrngd  20255  isdrngdOLD  20257  subrgmcl  20282  subrgunit  20288  issubdrg  20296  lmodprop2d  20441  qsssubdrg  20893  psraddcl  21388  psrmulcllem  21392  psrvscacl  21398  mhppwdeg  21577  matgsum  21823  mat1rhmcl  21867  dmatmulcl  21886  scmatghm  21919  imacmp  22785  prdstps  23017  symgtgp  23494  prdstgpd  23513  tsmssub  23537  ustuqtop3  23632  utop2nei  23639  xpsxmetlem  23769  xpsmet  23772  imasf1oxms  23882  imasf1oms  23883  prdsmslem1  23920  prdsxmslem1  23921  prdsxmslem2  23922  tngngp2  24053  cnmpopc  24328  caublcls  24710  minveclem3a  24828  efsubm  25944  wlkl1loop  28649  wlkres  28681  clwwlknonex2lem1  29114  eucrct2eupth  29252  cyc3co2  32059  sdrgdvcl  32145  sdrginvcl  32146  drgextlsp  32379  fedgmullem2  32412  cvmliftlem7  33972  cvmliftlem10  33975  ex-sategoelel  34102  ex-sategoelelomsuc  34107  prdsbnd  36325  prdstotbnd  36326  prdsbnd2  36327  cnpwstotbnd  36329  repwsmet  36366  diblss  39706  kelac1  41448  omcl2  41726  ofoafg  41747  naddwordnexlem0  41790  naddwordnexlem3  41793  iunrelexpuztr  42113  mnuprdlem3  42676  fnchoice  43356  sumnnodd  43991  sublimc  44013  divlimc  44017  cncfshiftioo  44253  itgperiod  44342  stoweidlem26  44387  dirkercncflem2  44465  fourierdlem32  44500  fourierdlem33  44501  fourierdlem46  44513  fourierdlem48  44515  fourierdlem49  44516  fourierdlem62  44529  fourierdlem74  44541  fourierdlem75  44542  fourierdlem76  44543  fourierdlem81  44548  fourierdlem88  44555  fourierdlem89  44556  fourierdlem91  44558  fourierdlem93  44560  fourierdlem103  44570  fourierdlem104  44571  fouriersw  44592  fouriercn  44593  smfco  45163  uspgropssxp  46166  issubmgm2  46204  rnghmsubcsetclem1  46393  rnghmsubcsetclem2  46394  rngccatidALTV  46407  funcrngcsetc  46416  rhmsubcsetclem1  46439  rhmsubcsetclem2  46440  rhmsubcrngclem1  46445  rhmsubcrngclem2  46446  funcringcsetc  46453  ringccatidALTV  46470  srhmsubc  46494  rhmsubclem3  46506  rhmsubclem4  46507  srhmsubcALTV  46512  rhmsubcALTVlem3  46524  rhmsubcALTVlem4  46525  ovmpordxf  46534  indthinc  47192  indthincALT  47193  mndtccatid  47233