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 ⊢ (𝜑 → 𝐶 ∈ 𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  ovmpodxf  6214  nnaordi  6781  iccf1o  10407  infssfzcldc  10669  ccatw2s1p1g  11413  nnmindc  12811  ennnfonelemrn  13310  ctiunctlemfo  13330  sgrppropd  13728  mndpropd  13753  issubmnd  13755  imasgrp  13914  mulgnndir  13954  subg0cl  13985  subginvcl  13986  subgcl  13987  rngcl  14243  rngpropd  14254  srgcl  14274  srgidcl  14280  ringidcl  14325  ringpropd  14343  dvdsrd  14401  dvrvald  14441  subrngmcl  14517  subrgmcl  14541  subrgunit  14547  lmodprop2d  14685  lidl0  14826  lidl1  14827  psraddcl  15071  wlkl1loop  16599  wlkres  16620  clwwlknonex2lem1  16678