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

Definition df-pr 3379
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 3443. For a more traditional definition, but requiring a dummy variable, see dfpr2 3391. (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 3373 . 2 class {𝐴, 𝐵}
41csn 3372 . . 3 class {𝐴}
52csn 3372 . . 3 class {𝐵}
64, 5cun 2912 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1243 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3386  dfpr2  3391  ralprg  3418  rexprg  3419  disjpr2  3431  prcom  3443  preq1  3444  qdass  3464  qdassr  3465  tpidm12  3466  prprc1  3475  difprsn1  3500  diftpsn3  3502  snsspr1  3509  snsspr2  3510  prss  3517  prssg  3518  2ordpr  4236  xpsspw  4428  dmpropg  4771  rnpropg  4778  funprg  4927  funtp  4930  fntpg  4933  f1oprg  5146  fnimapr  5211  fpr  5323  fprg  5324  fmptpr  5333  fvpr1  5343  fvpr1g  5345  fvpr2g  5346  df2o3  5992  fzosplitprm1  9048  bdcpr  9855
  Copyright terms: Public domain W3C validator