![]() |
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 4770 | . 2 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸}) |
3 | tpeq123d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | tpeq2d 4771 | . 2 ⊢ (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸}) |
5 | tpeq123d.3 | . . 3 ⊢ (𝜑 → 𝐸 = 𝐹) | |
6 | 5 | tpeq3d 4772 | . 2 ⊢ (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹}) |
7 | 2, 4, 6 | 3eqtrd 2784 | 1 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 {ctp 4652 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-tru 1540 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-v 3490 df-un 3981 df-sn 4649 df-pr 4651 df-tp 4653 |
This theorem is referenced by: fz0tp 13685 fz0to5un2tp 13688 fzo0to3tp 13802 fzo1to4tp 13804 prdsval 17515 imasval 17571 fucval 18027 fucpropd 18047 setcval 18144 catcval 18167 estrcval 18192 xpcval 18246 efmnd 18905 dfcnfldOLD 21403 psrval 21958 om1val 25082 s3rnOLD 32912 rlocval 33231 idlsrgval 33496 ldualset 39081 erngfset 40756 erngfset-rN 40764 dvafset 40961 dvaset 40962 dvhfset 41037 dvhset 41038 hlhilset 41891 rabren3dioph 42771 mendval 43140 oaun3 43344 nnsum4primesodd 47670 nnsum4primesoddALTV 47671 rngcvalALTV 47988 ringcvalALTV 48012 mndtcval 48752 |
Copyright terms: Public domain | W3C validator |