![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tprot | Structured version Visualization version GIF version |
Description: Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.) |
Ref | Expression |
---|---|
tprot | ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3orrot 1092 | . . 3 ⊢ ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)) | |
2 | 1 | abbii 2801 | . 2 ⊢ {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)} |
3 | dftp2 4686 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} | |
4 | dftp2 4686 | . 2 ⊢ {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)} | |
5 | 2, 3, 4 | 3eqtr4i 2769 | 1 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} |
Colors of variables: wff setvar class |
Syntax hints: ∨ w3o 1086 = wceq 1541 {cab 2708 {ctp 4626 |
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-or 846 df-3or 1088 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-un 3949 df-sn 4623 df-pr 4625 df-tp 4627 |
This theorem is referenced by: tpcomb 4748 tpass 4749 tpidm13 4753 tpidm23 4754 tpprceq3 4800 fvtp2 7181 fvtp3 7182 fvtp2g 7184 fvtp3g 7185 f13dfv 7256 en3lplem2 9590 estrres 18073 nb3grprlem2 28503 nb3grpr 28504 nb3grpr2 28505 nb3gr2nb 28506 cplgr3v 28557 frgr3v 29393 1to3vfriswmgr 29398 dvh4dimN 40123 en3lplem2VD 43376 |
Copyright terms: Public domain | W3C validator |