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  6786  iccf1o  10423  infssfzcldc  10685  ccatw2s1p1g  11434  nnmindc  12835  ennnfonelemrn  13367  ctiunctlemfo  13387  sgrppropd  13786  mndpropd  13811  issubmnd  13813  imasgrp  13972  mulgnndir  14012  subg0cl  14043  subginvcl  14044  subgcl  14045  rngcl  14349  rngpropd  14360  srgcl  14380  srgidcl  14386  ringidcl  14431  ringpropd  14449  dvdsrd  14509  dvrvald  14549  subrngmcl  14625  subrgmcl  14649  subrgunit  14655  lmodprop2d  14793  lidl0  14934  lidl1  14935  psraddcl  15193  psrmulclfilem  15198  wlkl1loop  16821  wlkres  16842  clwwlknonex2lem1  16900