![]() |
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 2834 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷) |
5 | 1, 4 | eqeltrrd 2833 | 1 ⊢ (𝜑 → 𝐶 ∈ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2106 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2723 df-clel 2809 |
This theorem is referenced by: axcc2lem 10413 axcclem 10434 icoshftf1o 13433 lincmb01cmp 13454 fzosubel 13673 symgsubmefmndALT 19235 psgnunilem1 19325 efgcpbllemb 19587 lspprabs 20655 cnmpt2res 23110 xpstopnlem1 23242 tususp 23706 tustps 23707 ressxms 23963 ressms 23964 tmsxpsval 23976 limcco 25339 dvcnp2 25366 dvcnvlem 25422 taylthlem2 25815 jensen 26420 f1otrg 27987 nsgqusf1olem1 32380 txomap 32643 probmeasb 33258 fsum2dsub 33448 cvmlift2lem9 34131 prdsbnd2 36466 iocopn 44004 icoopn 44009 reclimc 44140 cncfiooicclem1 44380 itgiccshift 44467 dirkercncflem4 44593 fourierdlem32 44626 fourierdlem33 44627 fourierdlem60 44653 fourierdlem61 44654 fourierdlem76 44669 fourierdlem81 44674 fourierdlem90 44683 fourierdlem111 44704 |
Copyright terms: Public domain | W3C validator |