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  10417  infssfzcldc  10679  ccatw2s1p1g  11427  nnmindc  12827  ennnfonelemrn  13359  ctiunctlemfo  13379  sgrppropd  13777  mndpropd  13802  issubmnd  13804  imasgrp  13963  mulgnndir  14003  subg0cl  14034  subginvcl  14035  subgcl  14036  rngcl  14292  rngpropd  14303  srgcl  14323  srgidcl  14329  ringidcl  14374  ringpropd  14392  dvdsrd  14450  dvrvald  14490  subrngmcl  14566  subrgmcl  14590  subrgunit  14596  lmodprop2d  14734  lidl0  14875  lidl1  14876  psraddcl  15120  wlkl1loop  16697  wlkres  16718  clwwlknonex2lem1  16776