Theorem 3eltr4d 2851

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811

This theorem is referenced by:  elimdelov  7454  ovmpodxf  7508  cantnflt  9581  cantnflem1  9598  cofsmo  10179  cfsmolem  10180  axcclem  10367  smobeth  10497  iccf1o  13412  ccatw2s1p1  14560  revccat  14689  pwp1fsum  16318  vdwlem8  16916  issubc3  17773  cofucl  17812  catccatid  18030  xpccatid  18111  issstrmgm  18578  issubmgm2  18628  sgrppropd  18656  mndpropd  18684  issubmnd  18686  pwspjmhm  18755  gsumsgrpccat  18765  smndex1gbas  18827  pwmnd  18862  imasgrp  18986  mulgnndir  19033  subg0cl  19064  subginvcl  19065  subgcl  19066  psgnunilem2  19424  finodsubmsubg  19496  efgsp1  19666  gsumzsubmcl  19847  dpjghm  19994  pwsco1rhm  20435  pwsco2rhm  20436  subrngmcl  20490  subrgunit  20523  rnghmsubcsetclem1  20564  rnghmsubcsetclem2  20565  funcrngcsetc  20573  rhmsubcsetclem1  20593  rhmsubcsetclem2  20594  rhmsubcrngclem1  20599  rhmsubcrngclem2  20600  funcringcsetc  20607  srhmsubc  20613  rhmsubclem3  20620  rhmsubclem4  20621  isdrngd  20698  isdrngdOLD  20700  issubdrg  20713  lmodprop2d  20875  rngqiprngimfo  21256  qsssubdrg  21381  pzriprnglem4  21439  pzriprnglem5  21440  psraddcl  21894  psraddclOLD  21895  psrmulcllem  21901  psrvscacl  21907  mhppwdeg  22093  psdcl  22104  matgsum  22381  mat1rhmcl  22425  dmatmulcl  22444  scmatghm  22477  imacmp  23341  prdstps  23573  symgtgp  24050  prdstgpd  24069  tsmssub  24093  ustuqtop3  24187  utop2nei  24194  xpsxmetlem  24323  xpsmet  24326  imasf1oxms  24433  imasf1oms  24434  prdsmslem1  24471  prdsxmslem1  24472  prdsxmslem2  24473  tngngp2  24596  cnmpopc  24878  caublcls  25265  minveclem3a  25383  efsubm  26516  negleft  28054  negright  28055  noseqrdg0  28303  wlkl1loop  29711  wlkres  29742  clwwlknonex2lem1  30182  eucrct2eupth  30320  subgmulgcld  33126  cyc3co2  33222  sdrgdvcl  33381  sdrginvcl  33382  drgextlsp  33750  fedgmullem2  33787  algextdeglem4  33877  cvmliftlem7  35485  cvmliftlem10  35488  ex-sategoelel  35615  ex-sategoelelomsuc  35620  prdsbnd  37994  prdstotbnd  37995  prdsbnd2  37996  cnpwstotbnd  37998  repwsmet  38035  diblss  41440  kelac1  43315  omcl2  43585  ofoafg  43606  naddwordnexlem0  43648  naddwordnexlem3  43651  iunrelexpuztr  43970  mnuprdlem3  44525  fnchoice  45284  sumnnodd  45886  sublimc  45906  divlimc  45910  cncfshiftioo  46146  itgperiod  46235  stoweidlem26  46280  dirkercncflem2  46358  fourierdlem32  46393  fourierdlem33  46394  fourierdlem46  46406  fourierdlem48  46408  fourierdlem49  46409  fourierdlem62  46422  fourierdlem74  46434  fourierdlem75  46435  fourierdlem76  46436  fourierdlem81  46441  fourierdlem88  46448  fourierdlem89  46449  fourierdlem91  46451  fourierdlem93  46453  fourierdlem103  46463  fourierdlem104  46464  fouriersw  46485  fouriercn  46486  smfco  47056  uspgropssxp  48400  rngccatidALTV  48528  rhmsubcALTVlem3  48539  rhmsubcALTVlem4  48540  ringccatidALTV  48562  srhmsubcALTV  48581  ovmpordxf  48595  discsubc  49319  imaf1co  49410  tposcurf2cl  49557  fuco2eld  49568  fuco22natlem  49600  indthinc  49717  indthincALT  49718  mndtccatid  49842