MPE Home 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