![]() |
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 3563. For a more traditional definition, but requiring a dummy variable, see dfpr2 3510. (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 3492 | . 2 class {𝐴, 𝐵} |
4 | 1 | csn 3491 | . . 3 class {𝐴} |
5 | 2 | csn 3491 | . . 3 class {𝐵} |
6 | 4, 5 | cun 3033 | . 2 class ({𝐴} ∪ {𝐵}) |
7 | 3, 6 | wceq 1312 | 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
Colors of variables: wff set class |
This definition is referenced by: dfsn2 3505 dfpr2 3510 ralprg 3538 rexprg 3539 disjpr2 3551 prcom 3563 preq1 3564 qdass 3584 qdassr 3585 tpidm12 3586 prprc1 3595 difprsn1 3623 diftpsn3 3625 difpr 3626 snsspr1 3632 snsspr2 3633 prss 3640 prssg 3641 iunxprg 3857 2ordpr 4397 xpsspw 4609 dmpropg 4967 rnpropg 4974 funprg 5129 funtp 5132 fntpg 5135 f1oprg 5363 fnimapr 5433 fpr 5554 fprg 5555 fmptpr 5564 fvpr1 5576 fvpr1g 5578 fvpr2g 5579 df2o3 6279 unfiexmid 6757 prfidisj 6766 pr2nelem 6994 xp2dju 7016 fzosplitprm1 9898 hashprg 10441 sumpr 11068 strle2g 11887 bdcpr 12752 |
Copyright terms: Public domain | W3C validator |