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

Definition df-pr 3413
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 3476. For a more traditional definition, but requiring a dummy variable, see dfpr2 3425. (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 3407 . 2 class {𝐴, 𝐵}
41csn 3406 . . 3 class {𝐴}
52csn 3406 . . 3 class {𝐵}
64, 5cun 2972 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1285 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3420  dfpr2  3425  ralprg  3451  rexprg  3452  disjpr2  3464  prcom  3476  preq1  3477  qdass  3497  qdassr  3498  tpidm12  3499  prprc1  3508  difprsn1  3533  diftpsn3  3535  snsspr1  3541  snsspr2  3542  prss  3549  prssg  3550  2ordpr  4275  xpsspw  4478  dmpropg  4823  rnpropg  4830  funprg  4980  funtp  4983  fntpg  4986  f1oprg  5199  fnimapr  5265  fpr  5377  fprg  5378  fmptpr  5387  fvpr1  5397  fvpr1g  5399  fvpr2g  5400  df2o3  6078  unfiexmid  6438  pr2nelem  6519  fzosplitprm1  9320  sizeprg  9832  bdcpr  10820
  Copyright terms: Public domain W3C validator