Theorem 3eltr4d 2322

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  ovmpodxf  6204  nnaordi  6771  iccf1o  10386  infssfzcldc  10647  ccatw2s1p1g  11391  nnmindc  12789  ennnfonelemrn  13288  ctiunctlemfo  13308  sgrppropd  13705  mndpropd  13730  issubmnd  13732  imasgrp  13891  mulgnndir  13931  subg0cl  13962  subginvcl  13963  subgcl  13964  rngcl  14218  rngpropd  14229  srgcl  14248  srgidcl  14254  ringidcl  14298  ringpropd  14316  dvdsrd  14374  dvrvald  14414  subrngmcl  14490  subrgmcl  14514  subrgunit  14520  lmodprop2d  14657  lidl0  14798  lidl1  14799  psraddcl  14994  wlkl1loop  16513  wlkres  16534  clwwlknonex2lem1  16592