![]() |
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 3683. For a more traditional definition, but requiring a dummy variable, see dfpr2 3626. (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 3608 | . 2 class {𝐴, 𝐵} |
4 | 1 | csn 3607 | . . 3 class {𝐴} |
5 | 2 | csn 3607 | . . 3 class {𝐵} |
6 | 4, 5 | cun 3142 | . 2 class ({𝐴} ∪ {𝐵}) |
7 | 3, 6 | wceq 1364 | 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
Colors of variables: wff set class |
This definition is referenced by: dfsn2 3621 dfpr2 3626 ralprg 3658 rexprg 3659 disjpr2 3671 prcom 3683 preq1 3684 qdass 3704 qdassr 3705 tpidm12 3706 prprc1 3715 difprsn1 3746 diftpsn3 3748 difpr 3749 snsspr1 3755 snsspr2 3756 prss 3763 prssg 3764 iunxprg 3982 2ordpr 4541 xpsspw 4756 dmpropg 5119 rnpropg 5126 funprg 5285 funtp 5288 fntpg 5291 f1oprg 5524 fnimapr 5597 fpr 5719 fprg 5720 fmptpr 5729 fvpr1 5741 fvpr1g 5743 fvpr2g 5744 df2o3 6456 enpr2d 6844 unfiexmid 6947 prfidisj 6956 pr2nelem 7221 xp2dju 7245 fzosplitprm1 10266 hashprg 10823 sumpr 11456 strle2g 12622 bdcpr 15101 |
Copyright terms: Public domain | W3C validator |