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 1088 | . . 3 ⊢ ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)) | |
2 | 1 | abbii 2889 | . 2 ⊢ {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)} |
3 | dftp2 4630 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} | |
4 | dftp2 4630 | . 2 ⊢ {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)} | |
5 | 2, 3, 4 | 3eqtr4i 2857 | 1 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} |
Colors of variables: wff setvar class |
Syntax hints: ∨ w3o 1082 = wceq 1536 {cab 2802 {ctp 4574 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-v 3499 df-un 3944 df-sn 4571 df-pr 4573 df-tp 4575 |
This theorem is referenced by: tpcomb 4690 tpass 4691 tpidm13 4695 tpidm23 4696 tpprceq3 4740 fvtp2 6961 fvtp3 6962 fvtp2g 6964 fvtp3g 6965 f13dfv 7034 en3lplem2 9079 estrres 17392 nb3grprlem2 27166 nb3grpr 27167 nb3grpr2 27168 nb3gr2nb 27169 cplgr3v 27220 frgr3v 28057 1to3vfriswmgr 28062 dvh4dimN 38587 en3lplem2VD 41184 |
Copyright terms: Public domain | W3C validator |