![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3eltr4g | Structured version Visualization version GIF version |
Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
Ref | Expression |
---|---|
3eltr4g.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐵) |
3eltr4g.2 | ⊢ 𝐶 = 𝐴 |
3eltr4g.3 | ⊢ 𝐷 = 𝐵 |
Ref | Expression |
---|---|
3eltr4g | ⊢ (𝜑 → 𝐶 ∈ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eltr4g.2 | . . 3 ⊢ 𝐶 = 𝐴 | |
2 | 3eltr4g.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐵) | |
3 | 1, 2 | syl5eqel 2910 | . 2 ⊢ (𝜑 → 𝐶 ∈ 𝐵) |
4 | 3eltr4g.3 | . 2 ⊢ 𝐷 = 𝐵 | |
5 | 3, 4 | syl6eleqr 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 |