Theorem 3eltr4d 2843

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  elimdelov  7465  ovmpodxf  7519  cantnflt  9601  cantnflem1  9618  cofsmo  10198  cfsmolem  10199  axcclem  10386  smobeth  10515  iccf1o  13433  ccatw2s1p1  14577  revccat  14707  pwp1fsum  16337  vdwlem8  16935  issubc3  17791  cofucl  17830  catccatid  18048  xpccatid  18129  issstrmgm  18562  issubmgm2  18612  sgrppropd  18640  mndpropd  18668  issubmnd  18670  pwspjmhm  18739  gsumsgrpccat  18749  smndex1gbas  18811  pwmnd  18846  imasgrp  18970  mulgnndir  19017  subg0cl  19048  subginvcl  19049  subgcl  19050  psgnunilem2  19409  finodsubmsubg  19481  efgsp1  19651  gsumzsubmcl  19832  dpjghm  19979  pwsco1rhm  20422  pwsco2rhm  20423  subrngmcl  20477  subrgunit  20510  rnghmsubcsetclem1  20551  rnghmsubcsetclem2  20552  funcrngcsetc  20560  rhmsubcsetclem1  20580  rhmsubcsetclem2  20581  rhmsubcrngclem1  20586  rhmsubcrngclem2  20587  funcringcsetc  20594  srhmsubc  20600  rhmsubclem3  20607  rhmsubclem4  20608  isdrngd  20685  isdrngdOLD  20687  issubdrg  20700  lmodprop2d  20862  rngqiprngimfo  21243  qsssubdrg  21368  pzriprnglem4  21426  pzriprnglem5  21427  psraddcl  21880  psraddclOLD  21881  psrmulcllem  21887  psrvscacl  21893  mhppwdeg  22070  psdcl  22081  matgsum  22357  mat1rhmcl  22401  dmatmulcl  22420  scmatghm  22453  imacmp  23317  prdstps  23549  symgtgp  24026  prdstgpd  24045  tsmssub  24069  ustuqtop3  24164  utop2nei  24171  xpsxmetlem  24300  xpsmet  24303  imasf1oxms  24410  imasf1oms  24411  prdsmslem1  24448  prdsxmslem1  24449  prdsxmslem2  24450  tngngp2  24573  cnmpopc  24855  caublcls  25242  minveclem3a  25360  efsubm  26493  noseqrdg0  28241  wlkl1loop  29618  wlkres  29649  clwwlknonex2lem1  30086  eucrct2eupth  30224  subgmulgcld  33027  cyc3co2  33112  sdrgdvcl  33265  sdrginvcl  33266  drgextlsp  33582  fedgmullem2  33619  algextdeglem4  33703  cvmliftlem7  35271  cvmliftlem10  35274  ex-sategoelel  35401  ex-sategoelelomsuc  35406  prdsbnd  37780  prdstotbnd  37781  prdsbnd2  37782  cnpwstotbnd  37784  repwsmet  37821  diblss  41157  kelac1  43045  omcl2  43315  ofoafg  43336  naddwordnexlem0  43378  naddwordnexlem3  43381  iunrelexpuztr  43701  mnuprdlem3  44256  fnchoice  45016  sumnnodd  45621  sublimc  45643  divlimc  45647  cncfshiftioo  45883  itgperiod  45972  stoweidlem26  46017  dirkercncflem2  46095  fourierdlem32  46130  fourierdlem33  46131  fourierdlem46  46143  fourierdlem48  46145  fourierdlem49  46146  fourierdlem62  46159  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem81  46178  fourierdlem88  46185  fourierdlem89  46186  fourierdlem91  46188  fourierdlem93  46190  fourierdlem103  46200  fourierdlem104  46201  fouriersw  46222  fouriercn  46223  smfco  46793  uspgropssxp  48125  rngccatidALTV  48253  rhmsubcALTVlem3  48264  rhmsubcALTVlem4  48265  ringccatidALTV  48287  srhmsubcALTV  48306  ovmpordxf  48320  discsubc  49046  imaf1co  49137  tposcurf2cl  49284  fuco2eld  49295  fuco22natlem  49327  indthinc  49444  indthincALT  49445  mndtccatid  49569