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

Definition df-pr 3374
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 3437. For a more traditional definition, but requiring a dummy variable, see dfpr2 3383. (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 3368 . 2 class {A, B}
41csn 3367 . . 3 class {A}
52csn 3367 . . 3 class {B}
64, 5cun 2909 . 2 class ({A} ∪ {B})
73, 6wceq 1242 1 wff {A, B} = ({A} ∪ {B})
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3381  dfpr2  3383  ralprg  3412  rexprg  3413  disjpr2  3425  prcom  3437  preq1  3438  qdass  3458  qdassr  3459  tpidm12  3460  prprc1  3469  difprsn1  3494  diftpsn3  3496  snsspr1  3503  snsspr2  3504  prss  3511  prssg  3512  onsucelsucexmidlem  4214  xpsspw  4393  dmpropg  4736  rnpropg  4743  funprg  4892  funtp  4895  fntpg  4898  f1oprg  5111  fnimapr  5176  fpr  5288  fprg  5289  fmptpr  5298  fvpr1  5308  fvpr1g  5310  fvpr2g  5311  df2o3  5953  fzosplitprm1  8860  bdcpr  9326
  Copyright terms: Public domain W3C validator