Theorem 3eltr4d 2878

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  elimdelov  7506  ovmpodxf  7560  cantnflt  9637  cantnflem1  9654  cofsmo  10248  cfsmolem  10249  axcclem  10436  smobeth  10566  iccf1o  13518  ccatw2s1p1  14670  revccat  14799  pwp1fsum  16444  vdwlem8  17043  issubc3  17901  cofucl  17940  catccatid  18158  xpccatid  18239  issstrmgm  18706  issubmgm2  18756  sgrppropd  18784  mndpropd  18812  issubmnd  18814  pwspjmhm  18884  gsumsgrpccat  18894  smndex1gbas  18956  smndex1gbasOLD  18957  pwmnd  18994  imasgrp  19117  mulgnndir  19164  subg0cl  19195  subginvcl  19196  subgcl  19197  psgnunilem2  19560  finodsubmsubg  19632  efgsp1  19802  gsumzsubmcl  19983  dpjghm  20130  pwsco1rhm  20589  pwsco2rhm  20590  subrngmcl  20656  subrgunit  20689  rnghmsubcsetclem1  20730  rnghmsubcsetclem2  20731  funcrngcsetc  20739  rhmsubcsetclem1  20759  rhmsubcsetclem2  20760  rhmsubcrngclem1  20765  rhmsubcrngclem2  20766  funcringcsetc  20773  srhmsubc  20779  rhmsubclem3  20786  rhmsubclem4  20787  isdrngd  20868  isdrngdOLD  20870  issubdrg  20883  lmodprop2d  21045  rngqiprngimfo  21441  qsssubdrg  21576  pzriprnglem4  21634  pzriprnglem5  21635  psraddcl  22089  psrmulcllem  22095  psrvscacl  22101  mhppwdeg  22313  psdcl  22324  matgsum  22594  mat1rhmcl  22638  dmatmulcl  22657  scmatghm  22690  imacmp  23554  prdstps  23786  symgtgp  24263  prdstgpd  24282  tsmssub  24306  ustuqtop3  24400  utop2nei  24407  xpsxmetlem  24536  xpsmet  24539  imasf1oxms  24646  imasf1oms  24647  prdsmslem1  24684  prdsxmslem1  24685  prdsxmslem2  24686  tngngp2  24809  cnmpopc  25087  caublcls  25468  minveclem3a  25586  efsubm  26716  negleft  28251  negright  28252  noseqrdg0  28500  wlkl1loop  29987  wlkres  30018  clwwlknonex2lem1  30458  eucrct2eupth  30596  subgmulgcld  33363  cyc3co2  33460  sdrgdvcl  33620  sdrginvcl  33621  drgextlsp  33984  fedgmullem2  34020  algextdeglem4  34110  cvmliftlem7  35783  cvmliftlem10  35786  ex-sategoelel  35913  ex-sategoelelomsuc  35918  nadddilem1  36712  nadddilem2  36713  nadddilem3  36714  nadddilem4  36715  prdsbnd  38464  prdstotbnd  38465  prdsbnd2  38466  cnpwstotbnd  38468  repwsmet  38505  diblss  41964  kelac1  43810  omcl2  44080  ofoafg  44101  naddwordnexlem0  44143  naddwordnexlem3  44146  iunrelexpuztr  44465  mnuprdlem3  45004  fnchoice  45769  sumnnodd  46366  sublimc  46386  divlimc  46390  cncfshiftioo  46626  itgperiod  46715  stoweidlem26  46760  dirkercncflem2  46838  fourierdlem32  46873  fourierdlem33  46874  fourierdlem46  46886  fourierdlem48  46888  fourierdlem49  46889  fourierdlem62  46902  fourierdlem74  46914  fourierdlem75  46915  fourierdlem76  46916  fourierdlem81  46921  fourierdlem88  46928  fourierdlem89  46929  fourierdlem91  46931  fourierdlem93  46933  fourierdlem103  46943  fourierdlem104  46944  fouriersw  46965  fouriercn  46966  smfco  47536  uspgropssxp  48929  rngccatidALTV  49057  rhmsubcALTVlem3  49068  rhmsubcALTVlem4  49069  ringccatidALTV  49091  srhmsubcALTV  49110  ovmpordxf  49139  discsubc  49862  imaf1co  49953  tposcurf2cl  50100  fuco2eld  50111  fuco22natlem  50143  indthinc  50260  indthincALT  50261  mndtccatid  50385