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 2917 | . 2 ⊢ (𝜑 → 𝐶 ∈ 𝐵) |
4 | 3eltr4g.3 | . 2 ⊢ 𝐷 = 𝐵 | |
5 | 3, 4 | eleqtrrdi 2924 | 1 ⊢ (𝜑 → 𝐶 ∈ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2114 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-cleq 2814 df-clel 2893 |
This theorem is referenced by: riotacl2 7116 rankelun 9287 rankelpr 9288 rankelop 9289 cdivcncf 23508 rrx0el 23984 itg1addlem4 24283 cxpcn3 25315 bposlem4 25849 mirauto 26456 ldgenpisyslem1 31429 nosepdm 33195 relowlpssretop 34661 0prjspnlem 39360 mapfzcons 39405 fourierdlem62 42543 fourierdlem63 42544 line2x 44826 line2y 44827 |
Copyright terms: Public domain | W3C validator |