Theorem 3eltr4d 2315

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  ovmpodxf  6157  nnaordi  6719  iccf1o  10284  ccatw2s1p1g  11271  nnmindc  12668  ennnfonelemrn  13103  ctiunctlemfo  13123  sgrppropd  13559  mndpropd  13586  issubmnd  13588  imasgrp  13761  mulgnndir  13801  subg0cl  13832  subginvcl  13833  subgcl  13834  rngcl  14021  rngpropd  14032  srgcl  14047  srgidcl  14053  ringidcl  14097  ringpropd  14115  dvdsrd  14172  dvrvald  14212  subrngmcl  14287  subrgmcl  14311  subrgunit  14317  lmodprop2d  14427  lidl0  14568  lidl1  14569  psraddcl  14764  wlkl1loop  16282  wlkres  16303  clwwlknonex2lem1  16361