Theorem 3eltr4d 2880

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  elimdelov  7515  ovmpodxf  7569  cantnflt  9648  cantnflem1  9665  cofsmo  10268  cfsmolem  10269  axcclem  10456  smobeth  10588  iccf1o  13541  ccatw2s1p1  14696  revccat  14827  pwp1fsum  16473  vdwlem8  17072  issubc3  17930  cofucl  17969  catccatid  18187  xpccatid  18268  issstrmgm  18737  issubmgm2  18795  sgrppropd  18823  mndpropd  18854  issubmnd  18856  pwspjmhm  18928  gsumsgrpccat  18938  smndex1gbas  19000  smndex1gbasOLD  19001  pwmnd  19045  imasgrp  19168  mulgnndir  19215  subg0cl  19246  subginvcl  19247  subgcl  19248  psgnunilem2  19611  finodsubmsubg  19683  efgsp1  19853  gsumzsubmcl  20034  dpjghm  20181  pwsco1rhm  20641  pwsco2rhm  20642  subrngmcl  20708  subrgunit  20741  rnghmsubcsetclem1  20782  rnghmsubcsetclem2  20783  funcrngcsetc  20791  rhmsubcsetclem1  20811  rhmsubcsetclem2  20812  rhmsubcrngclem1  20817  rhmsubcrngclem2  20818  funcringcsetc  20825  srhmsubc  20831  rhmsubclem3  20838  rhmsubclem4  20839  isdrngd  20920  isdrngdOLD  20922  issubdrg  20935  lmodprop2d  21097  rngqiprngimfo  21493  qsssubdrg  21628  pzriprnglem4  21686  pzriprnglem5  21687  psraddcl  22141  psrmulcllem  22147  psrvscacl  22153  mhppwdeg  22365  psdcl  22376  matgsum  22646  mat1rhmcl  22690  dmatmulcl  22709  scmatghm  22742  imacmp  23606  prdstps  23839  symgtgp  24316  prdstgpd  24335  tsmssub  24359  ustuqtop3  24453  utop2nei  24460  xpsxmetlem  24589  xpsmet  24592  imasf1oxms  24699  imasf1oms  24700  prdsmslem1  24737  prdsxmslem1  24738  prdsxmslem2  24739  tngngp2  24862  cnmpopc  25140  caublcls  25521  minveclem3a  25639  efsubm  26769  negleft  28304  negright  28305  noseqrdg0  28553  wlkl1loop  30047  wlkres  30078  clwwlknonex2lem1  30527  eucrct2eupth  30669  subgmulgcld  33429  cyc3co2  33526  sdrgdvcl  33686  sdrginvcl  33687  drgextlsp  34050  fedgmullem2  34086  algextdeglem4  34176  cvmliftlem7  35822  cvmliftlem10  35825  ex-sategoelel  35952  ex-sategoelelomsuc  35957  nadddilem1  36751  nadddilem2  36752  nadddilem3  36753  nadddilem4  36754  prdsbnd  38504  prdstotbnd  38505  prdsbnd2  38506  cnpwstotbnd  38508  repwsmet  38545  diblss  42004  kelac1  43850  omcl2  44120  ofoafg  44141  naddwordnexlem0  44183  naddwordnexlem3  44186  iunrelexpuztr  44505  mnuprdlem3  45044  fnchoice  45809  sumnnodd  46406  sublimc  46426  divlimc  46430  cncfshiftioo  46666  itgperiod  46755  stoweidlem26  46800  dirkercncflem2  46878  fourierdlem32  46913  fourierdlem33  46914  fourierdlem46  46926  fourierdlem48  46928  fourierdlem49  46929  fourierdlem62  46942  fourierdlem74  46954  fourierdlem75  46955  fourierdlem76  46956  fourierdlem81  46961  fourierdlem88  46968  fourierdlem89  46969  fourierdlem91  46971  fourierdlem93  46973  fourierdlem103  46983  fourierdlem104  46984  fouriersw  47005  fouriercn  47006  smfco  47576  uspgropssxp  48969  rngccatidALTV  49096  rhmsubcALTVlem3  49107  rhmsubcALTVlem4  49108  ringccatidALTV  49130  srhmsubcALTV  49149  ovmpordxf  49178  discsubc  49901  imaf1co  49992  tposcurf2cl  50139  fuco2eld  50150  fuco22natlem  50182  indthinc  50299  indthincALT  50300  mndtccatid  50424