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

Theorem 3eltr4g 2923
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, 2syl5eqel 2910 . 2 (𝜑𝐶𝐵)
4 3eltr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eleqr 2917 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1656  wcel 2164
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818  df-clel 2821
This theorem is referenced by:  riotacl2  6884  rankelun  9019  rankelpr  9020  rankelop  9021  cdivcncf  23097  rrx0el  23573  itg1addlem4  23872  cxpcn3  24898  bposlem4  25432  mirauto  26003  ldgenpisyslem1  30767  nosepdm  32368  relowlpssretop  33756  mapfzcons  38122  fourierdlem62  41177  fourierdlem63  41178  line2x  43320  line2y  43321
  Copyright terms: Public domain W3C validator