![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tpeq123d | Structured version Visualization version GIF version |
Description: Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
Ref | Expression |
---|---|
tpeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
tpeq123d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
tpeq123d.3 | ⊢ (𝜑 → 𝐸 = 𝐹) |
Ref | Expression |
---|---|
tpeq123d | ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tpeq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | tpeq1d 4387 | . 2 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸}) |
3 | tpeq123d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | tpeq2d 4388 | . 2 ⊢ (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸}) |
5 | tpeq123d.3 | . . 3 ⊢ (𝜑 → 𝐸 = 𝐹) | |
6 | 5 | tpeq3d 4389 | . 2 ⊢ (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹}) |
7 | 2, 4, 6 | 3eqtrd 2762 | 1 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1596 {ctp 4289 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-v 3306 df-un 3685 df-sn 4286 df-pr 4288 df-tp 4290 |
This theorem is referenced by: fz0tp 12555 fz0to4untppr 12557 fzo0to3tp 12669 fzo1to4tp 12671 prdsval 16238 imasval 16294 fucval 16740 fucpropd 16759 setcval 16849 catcval 16868 estrcval 16886 xpcval 16939 symgval 17920 psrval 19485 om1val 22951 ldualset 34832 erngfset 36506 erngfset-rN 36514 dvafset 36711 dvaset 36712 dvhfset 36788 dvhset 36789 hlhilset 37645 rabren3dioph 37798 mendval 38172 nnsum4primesodd 42111 nnsum4primesoddALTV 42112 rngcvalALTV 42388 ringcvalALTV 42434 |
Copyright terms: Public domain | W3C validator |