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

Theorem 3eltr4g 2842
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 2829 . 2 (𝜑𝐶𝐵)
4 3eltr4g.3 . 2 𝐷 = 𝐵
53, 4eleqtrrdi 2836 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wcel 2098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802
This theorem is referenced by:  riotacl2  7392  rankelun  9897  rankelpr  9898  rankelop  9899  cdivcncf  24885  rrx0el  25370  itg1addlem4  25672  itg1addlem4OLD  25673  cxpcn3  26728  bposlem4  27265  nosepdm  27663  mirauto  28560  ldgenpisyslem1  33913  relowlpssretop  36974  0prjspnlem  42182  mapfzcons  42278  fourierdlem62  45694  fourierdlem63  45695  line2x  48013  line2y  48014
  Copyright terms: Public domain W3C validator