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  6217  nnaordi  6785  iccf1o  10424  infssfzcldc  10686  ccatw2s1p1g  11435  nnmindc  12836  ennnfonelemrn  13368  ctiunctlemfo  13388  sgrppropd  13787  mndpropd  13812  issubmnd  13814  imasgrp  13973  mulgnndir  14013  subg0cl  14044  subginvcl  14045  subgcl  14046  rngcl  14350  rngpropd  14361  srgcl  14381  srgidcl  14387  ringidcl  14432  ringpropd  14450  dvdsrd  14510  dvrvald  14550  subrngmcl  14626  subrgmcl  14650  subrgunit  14656  lmodprop2d  14794  lidl0  14935  lidl1  14936  psraddcl  15184  psrmulclfilem  15189  wlkl1loop  16804  wlkres  16825  clwwlknonex2lem1  16883