Theorem 3eltr4d 2854

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  elimdelov  7452  ovmpodxf  7506  cantnflt  9584  cantnflem1  9601  cofsmo  10182  cfsmolem  10183  axcclem  10370  smobeth  10500  iccf1o  13440  ccatw2s1p1  14590  revccat  14719  pwp1fsum  16351  vdwlem8  16950  issubc3  17807  cofucl  17846  catccatid  18064  xpccatid  18145  issstrmgm  18612  issubmgm2  18662  sgrppropd  18690  mndpropd  18718  issubmnd  18720  pwspjmhm  18789  gsumsgrpccat  18799  smndex1gbas  18861  smndex1gbasOLD  18862  pwmnd  18899  imasgrp  19023  mulgnndir  19070  subg0cl  19101  subginvcl  19102  subgcl  19103  psgnunilem2  19461  finodsubmsubg  19533  efgsp1  19703  gsumzsubmcl  19884  dpjghm  20031  pwsco1rhm  20473  pwsco2rhm  20474  subrngmcl  20529  subrgunit  20562  rnghmsubcsetclem1  20603  rnghmsubcsetclem2  20604  funcrngcsetc  20612  rhmsubcsetclem1  20632  rhmsubcsetclem2  20633  rhmsubcrngclem1  20638  rhmsubcrngclem2  20639  funcringcsetc  20646  srhmsubc  20652  rhmsubclem3  20659  rhmsubclem4  20660  isdrngd  20737  isdrngdOLD  20739  issubdrg  20752  lmodprop2d  20914  rngqiprngimfo  21294  qsssubdrg  21401  pzriprnglem4  21459  pzriprnglem5  21460  psraddcl  21914  psrmulcllem  21920  psrvscacl  21926  mhppwdeg  22138  psdcl  22149  matgsum  22420  mat1rhmcl  22464  dmatmulcl  22483  scmatghm  22516  imacmp  23380  prdstps  23612  symgtgp  24089  prdstgpd  24108  tsmssub  24132  ustuqtop3  24226  utop2nei  24233  xpsxmetlem  24362  xpsmet  24365  imasf1oxms  24472  imasf1oms  24473  prdsmslem1  24510  prdsxmslem1  24511  prdsxmslem2  24512  tngngp2  24635  cnmpopc  24913  caublcls  25294  minveclem3a  25412  efsubm  26533  negleft  28068  negright  28069  noseqrdg0  28317  wlkl1loop  29724  wlkres  29755  clwwlknonex2lem1  30195  eucrct2eupth  30333  subgmulgcld  33124  cyc3co2  33221  sdrgdvcl  33383  sdrginvcl  33384  drgextlsp  33778  fedgmullem2  33814  algextdeglem4  33904  cvmliftlem7  35519  cvmliftlem10  35522  ex-sategoelel  35649  ex-sategoelelomsuc  35654  prdsbnd  38160  prdstotbnd  38161  prdsbnd2  38162  cnpwstotbnd  38164  repwsmet  38201  diblss  41662  kelac1  43508  omcl2  43778  ofoafg  43799  naddwordnexlem0  43841  naddwordnexlem3  43844  iunrelexpuztr  44163  mnuprdlem3  44718  fnchoice  45477  sumnnodd  46075  sublimc  46095  divlimc  46099  cncfshiftioo  46335  itgperiod  46424  stoweidlem26  46469  dirkercncflem2  46547  fourierdlem32  46582  fourierdlem33  46583  fourierdlem46  46595  fourierdlem48  46597  fourierdlem49  46598  fourierdlem62  46611  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem81  46630  fourierdlem88  46637  fourierdlem89  46638  fourierdlem91  46640  fourierdlem93  46642  fourierdlem103  46652  fourierdlem104  46653  fouriersw  46674  fouriercn  46675  smfco  47245  uspgropssxp  48635  rngccatidALTV  48763  rhmsubcALTVlem3  48774  rhmsubcALTVlem4  48775  ringccatidALTV  48797  srhmsubcALTV  48816  ovmpordxf  48830  discsubc  49554  imaf1co  49645  tposcurf2cl  49792  fuco2eld  49803  fuco22natlem  49835  indthinc  49952  indthincALT  49953  mndtccatid  50077