![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-pr | GIF version |
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 3476. For a more traditional definition, but requiring a dummy variable, see dfpr2 3425. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-pr | ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cpr 3407 | . 2 class {𝐴, 𝐵} |
4 | 1 | csn 3406 | . . 3 class {𝐴} |
5 | 2 | csn 3406 | . . 3 class {𝐵} |
6 | 4, 5 | cun 2972 | . 2 class ({𝐴} ∪ {𝐵}) |
7 | 3, 6 | wceq 1285 | 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
Colors of variables: wff set class |
This definition is referenced by: dfsn2 3420 dfpr2 3425 ralprg 3451 rexprg 3452 disjpr2 3464 prcom 3476 preq1 3477 qdass 3497 qdassr 3498 tpidm12 3499 prprc1 3508 difprsn1 3533 diftpsn3 3535 snsspr1 3541 snsspr2 3542 prss 3549 prssg 3550 2ordpr 4275 xpsspw 4478 dmpropg 4823 rnpropg 4830 funprg 4980 funtp 4983 fntpg 4986 f1oprg 5199 fnimapr 5265 fpr 5377 fprg 5378 fmptpr 5387 fvpr1 5397 fvpr1g 5399 fvpr2g 5400 df2o3 6078 unfiexmid 6438 pr2nelem 6519 fzosplitprm1 9320 sizeprg 9832 bdcpr 10820 |
Copyright terms: Public domain | W3C validator |