Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3eltr3d | Structured version Visualization version GIF version |
Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Ref | Expression |
---|---|
3eltr3d.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐵) |
3eltr3d.2 | ⊢ (𝜑 → 𝐴 = 𝐶) |
3eltr3d.3 | ⊢ (𝜑 → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
3eltr3d | ⊢ (𝜑 → 𝐶 ∈ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eltr3d.2 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) | |
2 | 3eltr3d.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐵) | |
3 | 3eltr3d.3 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐷) | |
4 | 2, 3 | eleqtrd 2912 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷) |
5 | 1, 4 | eqeltrrd 2911 | 1 ⊢ (𝜑 → 𝐶 ∈ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 |
This theorem is referenced by: axcc2lem 9846 axcclem 9867 icoshftf1o 12848 lincmb01cmp 12869 fzosubel 13084 psgnunilem1 18550 efgcpbllemb 18810 lspprabs 19796 cnmpt2res 22213 xpstopnlem1 22345 tususp 22808 tustps 22809 ressxms 23062 ressms 23063 tmsxpsval 23075 limcco 24418 dvcnp2 24444 dvcnvlem 24500 taylthlem2 24889 jensen 25493 f1otrg 26584 txomap 30997 probmeasb 31587 fsum2dsub 31777 cvmlift2lem9 32455 prdsbnd2 34954 iocopn 41672 icoopn 41677 reclimc 41810 cncfiooicclem1 42052 itgiccshift 42141 dirkercncflem4 42268 fourierdlem32 42301 fourierdlem33 42302 fourierdlem60 42328 fourierdlem61 42329 fourierdlem76 42344 fourierdlem81 42349 fourierdlem90 42358 fourierdlem111 42379 |
Copyright terms: Public domain | W3C validator |