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  10418  infssfzcldc  10680  ccatw2s1p1g  11429  nnmindc  12830  ennnfonelemrn  13362  ctiunctlemfo  13382  sgrppropd  13781  mndpropd  13806  issubmnd  13808  imasgrp  13967  mulgnndir  14007  subg0cl  14038  subginvcl  14039  subgcl  14040  rngcl  14334  rngpropd  14345  srgcl  14365  srgidcl  14371  ringidcl  14416  ringpropd  14434  dvdsrd  14492  dvrvald  14532  subrngmcl  14608  subrgmcl  14632  subrgunit  14638  lmodprop2d  14776  lidl0  14917  lidl1  14918  psraddcl  15163  psrmulclfilem  15168  wlkl1loop  16778  wlkres  16799  clwwlknonex2lem1  16857