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

Definition df-pr 3498
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.)
Assertion
Ref Expression
df-pr {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

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