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 1397   ∈ 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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

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

This theorem is referenced by:  ovmpodxf  6147  nnaordi  6676  iccf1o  10239  ccatw2s1p1g  11226  nnmindc  12610  ennnfonelemrn  13045  ctiunctlemfo  13065  sgrppropd  13501  mndpropd  13528  issubmnd  13530  imasgrp  13703  mulgnndir  13743  subg0cl  13774  subginvcl  13775  subgcl  13776  rngcl  13963  rngpropd  13974  srgcl  13989  srgidcl  13995  ringidcl  14039  ringpropd  14057  dvdsrd  14114  dvrvald  14154  subrngmcl  14229  subrgmcl  14253  subrgunit  14259  lmodprop2d  14368  lidl0  14509  lidl1  14510  psraddcl  14700  wlkl1loop  16215  wlkres  16236  clwwlknonex2lem1  16294