![]() |
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 | eqeltrid 2894 | . 2 ⊢ (𝜑 → 𝐶 ∈ 𝐵) |
4 | 3eltr4g.3 | . 2 ⊢ 𝐷 = 𝐵 | |
5 | 3, 4 | eleqtrrdi 2901 | 1 ⊢ (𝜑 → 𝐶 ∈ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-cleq 2791 df-clel 2870 |
This theorem is referenced by: riotacl2 7109 rankelun 9285 rankelpr 9286 rankelop 9287 cdivcncf 23526 rrx0el 24002 itg1addlem4 24303 cxpcn3 25337 bposlem4 25871 mirauto 26478 ldgenpisyslem1 31532 nosepdm 33301 relowlpssretop 34781 0prjspnlem 39612 mapfzcons 39657 fourierdlem62 42810 fourierdlem63 42811 line2x 45168 line2y 45169 |
Copyright terms: Public domain | W3C validator |