| 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 2843 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷) |
| 5 | 1, 4 | eqeltrrd 2842 | 1 ⊢ (𝜑 → 𝐶 ∈ 𝐷) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-clel 2816 |
| This theorem is referenced by: axcc2lem 10476 axcclem 10497 icoshftf1o 13514 lincmb01cmp 13535 fzosubel 13763 symgsubmefmndALT 19421 psgnunilem1 19511 efgcpbllemb 19773 lspprabs 21094 cnmpt2res 23685 xpstopnlem1 23817 tususp 24281 tustps 24282 ressxms 24538 ressms 24539 tmsxpsval 24551 limcco 25928 dvcnp2 25955 dvcnp2OLD 25956 dvmulbr 25975 dvcobr 25983 dvcnvlem 26014 taylthlem2 26416 taylthlem2OLD 26417 jensen 27032 f1otrg 28879 nsgqusf1olem1 33441 txomap 33833 probmeasb 34432 fsum2dsub 34622 cvmlift2lem9 35316 prdsbnd2 37802 iocopn 45533 icoopn 45538 reclimc 45668 cncfiooicclem1 45908 itgiccshift 45995 dirkercncflem4 46121 fourierdlem32 46154 fourierdlem33 46155 fourierdlem60 46181 fourierdlem61 46182 fourierdlem76 46197 fourierdlem81 46202 fourierdlem90 46211 fourierdlem111 46232 fuco2eld3 49010 fucoid2 49044 |
| Copyright terms: Public domain | W3C validator |