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

Definition df-pr 3504
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 3569. For a more traditional definition, but requiring a dummy variable, see dfpr2 3516. (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 3498 . 2 class {𝐴, 𝐵}
41csn 3497 . . 3 class {𝐴}
52csn 3497 . . 3 class {𝐵}
64, 5cun 3039 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1316 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3511  dfpr2  3516  ralprg  3544  rexprg  3545  disjpr2  3557  prcom  3569  preq1  3570  qdass  3590  qdassr  3591  tpidm12  3592  prprc1  3601  difprsn1  3629  diftpsn3  3631  difpr  3632  snsspr1  3638  snsspr2  3639  prss  3646  prssg  3647  iunxprg  3863  2ordpr  4409  xpsspw  4621  dmpropg  4981  rnpropg  4988  funprg  5143  funtp  5146  fntpg  5149  f1oprg  5379  fnimapr  5449  fpr  5570  fprg  5571  fmptpr  5580  fvpr1  5592  fvpr1g  5594  fvpr2g  5595  df2o3  6295  enpr2d  6679  unfiexmid  6774  prfidisj  6783  pr2nelem  7015  xp2dju  7039  fzosplitprm1  9966  hashprg  10509  sumpr  11137  strle2g  11961  bdcpr  12965
  Copyright terms: Public domain W3C validator