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

Theorem 3eltr4g 2850
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 2837 . 2 (𝜑𝐶𝐵)
4 3eltr4g.3 . 2 𝐷 = 𝐵
53, 4eleqtrrdi 2844 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810
This theorem is referenced by:  riotacl2  7381  rankelun  9866  rankelpr  9867  rankelop  9868  cdivcncf  24436  rrx0el  24914  itg1addlem4  25215  itg1addlem4OLD  25216  cxpcn3  26253  bposlem4  26787  nosepdm  27184  mirauto  27932  ldgenpisyslem1  33156  relowlpssretop  36240  0prjspnlem  41366  mapfzcons  41444  fourierdlem62  44874  fourierdlem63  44875  line2x  47430  line2y  47431
  Copyright terms: Public domain W3C validator