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

Definition df-pr 3382
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 3446. For a more traditional definition, but requiring a dummy variable, see dfpr2 3394. (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 3376 . 2 class {𝐴, 𝐵}
41csn 3375 . . 3 class {𝐴}
52csn 3375 . . 3 class {𝐵}
64, 5cun 2915 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1243 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3389  dfpr2  3394  ralprg  3421  rexprg  3422  disjpr2  3434  prcom  3446  preq1  3447  qdass  3467  qdassr  3468  tpidm12  3469  prprc1  3478  difprsn1  3503  diftpsn3  3505  snsspr1  3512  snsspr2  3513  prss  3520  prssg  3521  2ordpr  4249  xpsspw  4450  dmpropg  4793  rnpropg  4800  funprg  4949  funtp  4952  fntpg  4955  f1oprg  5168  fnimapr  5233  fpr  5345  fprg  5346  fmptpr  5355  fvpr1  5365  fvpr1g  5367  fvpr2g  5368  df2o3  6014  fzosplitprm1  9090  bdcpr  9991
  Copyright terms: Public domain W3C validator