New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-pr | GIF version |
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, A ∈ { 1 , -u 1 } → (A ^ 2 ) = 1 (ex-pr in set.mm). They are unordered, so {A, B} = {B, A} as proven by prcom 3798. For a more traditional definition, but requiring a dummy variable, see dfpr2 3749. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-pr | ⊢ {A, B} = ({A} ∪ {B}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cB | . . 3 class B | |
3 | 1, 2 | cpr 3738 | . 2 class {A, B} |
4 | 1 | csn 3737 | . . 3 class {A} |
5 | 2 | csn 3737 | . . 3 class {B} |
6 | 4, 5 | cun 3207 | . 2 class ({A} ∪ {B}) |
7 | 3, 6 | wceq 1642 | 1 wff {A, B} = ({A} ∪ {B}) |
Colors of variables: wff setvar class |
This definition is referenced by: dfsn2 3747 dfpr2 3749 ralprg 3775 rexprg 3776 prcom 3798 preq1 3799 qdass 3819 qdassr 3820 tpidm12 3821 difprsn1 3847 diftpsn3 3849 snsspr1 3856 snsspr2 3857 prss 3861 prssg 3862 ssunpr 3868 sstp 3870 prex 4112 snprss1 4120 prprc2 4122 dmpropg 5068 funprg 5149 funprgOLD 5150 fnimapr 5374 fpr 5437 fvpr1 5449 1p1e2c 6155 el2c 6191 ce2 6192 |
Copyright terms: Public domain | W3C validator |