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

Definition df-pr 3353
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 3416. For a more traditional definition, but requiring a dummy variable, see dfpr2 3362. (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 3347 . 2 class {A, B}
41csn 3346 . . 3 class {A}
52csn 3346 . . 3 class {B}
64, 5cun 2888 . 2 class ({A} ∪ {B})
73, 6wceq 1226 1 wff {A, B} = ({A} ∪ {B})
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3360  dfpr2  3362  ralprg  3391  rexprg  3392  disjpr2  3404  prcom  3416  preq1  3417  qdass  3437  qdassr  3438  tpidm12  3439  prprc1  3448  difprsn1  3473  diftpsn3  3475  snsspr1  3482  snsspr2  3483  prss  3490  prssg  3491  onsucelsucexmidlem  4194  xpsspw  4373  dmpropg  4716  rnpropg  4723  funprg  4871  funtp  4874  fntpg  4877  f1oprg  5089  fnimapr  5154  fpr  5266  fprg  5267  fmptpr  5276  fvpr1  5286  fvpr1g  5288  fvpr2g  5289  df2o3  5925  bdcpr  7237
  Copyright terms: Public domain W3C validator