Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eltr4g Structured version   Visualization version   GIF version

Theorem 3eltr4g 2929
 Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
Hypotheses
Ref Expression
3eltr4g.1 (𝜑𝐴𝐵)
3eltr4g.2 𝐶 = 𝐴
3eltr4g.3 𝐷 = 𝐵
Assertion
Ref Expression
3eltr4g (𝜑𝐶𝐷)

Proof of Theorem 3eltr4g
StepHypRef Expression
1 3eltr4g.2 . . 3 𝐶 = 𝐴
2 3eltr4g.1 . . 3 (𝜑𝐴𝐵)
31, 2eqeltrid 2916 . 2 (𝜑𝐶𝐵)
4 3eltr4g.3 . 2 𝐷 = 𝐵
53, 4eleqtrrdi 2923 1 (𝜑𝐶𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2115 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2793 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2814  df-clel 2892 This theorem is referenced by:  riotacl2  7104  rankelun  9277  rankelpr  9278  rankelop  9279  cdivcncf  23504  rrx0el  23980  itg1addlem4  24281  cxpcn3  25315  bposlem4  25849  mirauto  26456  ldgenpisyslem1  31429  nosepdm  33195  relowlpssretop  34661  0prjspnlem  39407  mapfzcons  39452  fourierdlem62  42601  fourierdlem63  42602  line2x  44928  line2y  44929
 Copyright terms: Public domain W3C validator