ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-pr Structured version   GIF version

Definition df-pr 3347
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so {A, B} = {B, A} as proven by prcom 3410. For a more traditional definition, but requiring a dummy variable, see dfpr2 3356. (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 3341 . 2 class {A, B}
41csn 3340 . . 3 class {A}
52csn 3340 . . 3 class {B}
64, 5cun 2884 . 2 class ({A} ∪ {B})
73, 6wceq 1224 1 wff {A, B} = ({A} ∪ {B})
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3354  dfpr2  3356  ralprg  3385  rexprg  3386  disjpr2  3398  prcom  3410  preq1  3411  qdass  3431  qdassr  3432  tpidm12  3433  prprc1  3442  difprsn1  3467  diftpsn3  3469  snsspr1  3476  snsspr2  3477  prss  3484  prssg  3485  onsucelsucexmidlem  4187  xpsspw  4366  dmpropg  4709  rnpropg  4716  funprg  4864  funtp  4867  fntpg  4870  f1oprg  5082  fnimapr  5147  fpr  5259  fprg  5260  fmptpr  5269  fvpr1  5279  fvpr1g  5281  fvpr2g  5282  df2o3  5918  bdcpr  8328
  Copyright terms: Public domain W3C validator