![]() |
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 2829 | . 2 ⊢ (𝜑 → 𝐶 ∈ 𝐵) |
4 | 3eltr4g.3 | . 2 ⊢ 𝐷 = 𝐵 | |
5 | 3, 4 | eleqtrrdi 2836 | 1 ⊢ (𝜑 → 𝐶 ∈ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2717 df-clel 2802 |
This theorem is referenced by: riotacl2 7392 rankelun 9897 rankelpr 9898 rankelop 9899 cdivcncf 24885 rrx0el 25370 itg1addlem4 25672 itg1addlem4OLD 25673 cxpcn3 26728 bposlem4 27265 nosepdm 27663 mirauto 28560 ldgenpisyslem1 33913 relowlpssretop 36974 0prjspnlem 42182 mapfzcons 42278 fourierdlem62 45694 fourierdlem63 45695 line2x 48013 line2y 48014 |
Copyright terms: Public domain | W3C validator |