Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-pr | Unicode version |
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so as proven by prcom 3569. For a more traditional definition, but requiring a dummy variable, see dfpr2 3516. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-pr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | cpr 3498 | . 2 |
4 | 1 | csn 3497 | . . 3 |
5 | 2 | csn 3497 | . . 3 |
6 | 4, 5 | cun 3039 | . 2 |
7 | 3, 6 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: dfsn2 3511 dfpr2 3516 ralprg 3544 rexprg 3545 disjpr2 3557 prcom 3569 preq1 3570 qdass 3590 qdassr 3591 tpidm12 3592 prprc1 3601 difprsn1 3629 diftpsn3 3631 difpr 3632 snsspr1 3638 snsspr2 3639 prss 3646 prssg 3647 iunxprg 3863 2ordpr 4409 xpsspw 4621 dmpropg 4981 rnpropg 4988 funprg 5143 funtp 5146 fntpg 5149 f1oprg 5379 fnimapr 5449 fpr 5570 fprg 5571 fmptpr 5580 fvpr1 5592 fvpr1g 5594 fvpr2g 5595 df2o3 6295 enpr2d 6679 unfiexmid 6774 prfidisj 6783 pr2nelem 7015 xp2dju 7039 fzosplitprm1 9966 hashprg 10509 sumpr 11137 strle2g 11961 bdcpr 12965 |
Copyright terms: Public domain | W3C validator |