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 3599. For a more traditional definition, but requiring a dummy variable, see dfpr2 3546. (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 3528 | . 2 class {𝐴, 𝐵} |
4 | 1 | csn 3527 | . . 3 class {𝐴} |
5 | 2 | csn 3527 | . . 3 class {𝐵} |
6 | 4, 5 | cun 3069 | . 2 class ({𝐴} ∪ {𝐵}) |
7 | 3, 6 | wceq 1331 | 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
Colors of variables: wff set class |
This definition is referenced by: dfsn2 3541 dfpr2 3546 ralprg 3574 rexprg 3575 disjpr2 3587 prcom 3599 preq1 3600 qdass 3620 qdassr 3621 tpidm12 3622 prprc1 3631 difprsn1 3659 diftpsn3 3661 difpr 3662 snsspr1 3668 snsspr2 3669 prss 3676 prssg 3677 iunxprg 3893 2ordpr 4439 xpsspw 4651 dmpropg 5011 rnpropg 5018 funprg 5173 funtp 5176 fntpg 5179 f1oprg 5411 fnimapr 5481 fpr 5602 fprg 5603 fmptpr 5612 fvpr1 5624 fvpr1g 5626 fvpr2g 5627 df2o3 6327 enpr2d 6711 unfiexmid 6806 prfidisj 6815 pr2nelem 7047 xp2dju 7071 fzosplitprm1 10011 hashprg 10554 sumpr 11182 strle2g 12050 bdcpr 13069 |
Copyright terms: Public domain | W3C validator |