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

Theorem 3eltr4g 2856
 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 2843 . 2 (𝜑𝐶𝐵)
4 3eltr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eleqr 2850 1 (𝜑𝐶𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2139 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-clel 2756 This theorem is referenced by:  riotacl2  6788  rankelun  8910  rankelpr  8911  rankelop  8912  cdivcncf  22941  itg1addlem4  23685  cxpcn3  24709  bposlem4  25232  mirauto  25799  ldgenpisyslem1  30556  nosepdm  32161  relowlpssretop  33541  mapfzcons  37799  fourierdlem62  40906  fourierdlem63  40907
 Copyright terms: Public domain W3C validator