| 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 2809 | . 2 ⊢ {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)} |
| 3 | dftp2 4691 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} | |
| 4 | dftp2 4691 | . 2 ⊢ {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)} | |
| 5 | 2, 3, 4 | 3eqtr4i 2775 | 1 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} |
| Colors of variables: wff setvar class |
| Syntax hints: ∨ w3o 1086 = wceq 1540 {cab 2714 {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-3or 1088 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: tpcomb 4751 tpass 4752 tpidm13 4756 tpidm23 4757 tpprceq3 4804 fvtp2 7216 fvtp3 7217 fvtp2g 7219 fvtp3g 7220 f13dfv 7294 en3lplem2 9653 estrres 18184 nb3grprlem2 29398 nb3grpr 29399 nb3grpr2 29400 nb3gr2nb 29401 cplgr3v 29452 frgr3v 30294 1to3vfriswmgr 30299 dvh4dimN 41449 en3lplem2VD 44864 |
| Copyright terms: Public domain | W3C validator |