NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-pr GIF version

Definition df-pr 3742
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.)
Assertion
Ref Expression
df-pr {A, B} = ({A} ∪ {B})

Detailed syntax breakdown of Definition df-pr
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cpr 3738 . 2 class {A, B}
41csn 3737 . . 3 class {A}
52csn 3737 . . 3 class {B}
64, 5cun 3207 . 2 class ({A} ∪ {B})
73, 6wceq 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