| 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 4745 | . 2 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸}) |
| 3 | tpeq123d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
| 4 | 3 | tpeq2d 4746 | . 2 ⊢ (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸}) |
| 5 | tpeq123d.3 | . . 3 ⊢ (𝜑 → 𝐸 = 𝐹) | |
| 6 | 5 | tpeq3d 4747 | . 2 ⊢ (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹}) |
| 7 | 2, 4, 6 | 3eqtrd 2781 | 1 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹}) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 {ctp 4630 |
| 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-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-sn 4627 df-pr 4629 df-tp 4631 |
| This theorem is referenced by: fz0tp 13668 fz0to5un2tp 13671 fzo0to3tp 13791 fzo1to4tp 13793 prdsval 17500 imasval 17556 fucval 18006 fucpropd 18025 setcval 18122 catcval 18145 estrcval 18168 xpcval 18222 efmnd 18883 dfcnfldOLD 21380 psrval 21935 om1val 25063 s3rnOLD 32930 rlocval 33263 idlsrgval 33531 ldualset 39126 erngfset 40801 erngfset-rN 40809 dvafset 41006 dvaset 41007 dvhfset 41082 dvhset 41083 hlhilset 41936 rabren3dioph 42826 mendval 43191 oaun3 43395 nnsum4primesodd 47783 nnsum4primesoddALTV 47784 rngcvalALTV 48181 ringcvalALTV 48205 mndtcval 49176 |
| Copyright terms: Public domain | W3C validator |