![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > preq2 | GIF version |
Description: Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
preq2 | ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | preq1 3488 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) | |
2 | prcom 3487 | . 2 ⊢ {𝐶, 𝐴} = {𝐴, 𝐶} | |
3 | prcom 3487 | . 2 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶} | |
4 | 1, 2, 3 | 3eqtr4g 2140 | 1 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 {cpr 3418 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-v 2613 df-un 2987 df-sn 3423 df-pr 3424 |
This theorem is referenced by: preq12 3490 preq2i 3492 preq2d 3495 tpeq2 3498 preq12bg 3586 opeq2 3592 uniprg 3637 intprg 3690 prexg 3996 opth 4022 opeqsn 4037 relop 4537 funopg 4987 pr2ne 6606 hashprg 9918 bj-prexg 11006 |
Copyright terms: Public domain | W3C validator |