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

Definition df-pr 3438
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 3503. For a more traditional definition, but requiring a dummy variable, see dfpr2 3450. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-pr  |-  { A ,  B }  =  ( { A }  u.  { B } )

Detailed syntax breakdown of Definition df-pr
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cpr 3432 . 2  class  { A ,  B }
41csn 3431 . . 3  class  { A }
52csn 3431 . . 3  class  { B }
64, 5cun 2986 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1287 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3445  dfpr2  3450  ralprg  3478  rexprg  3479  disjpr2  3491  prcom  3503  preq1  3504  qdass  3524  qdassr  3525  tpidm12  3526  prprc1  3535  difprsn1  3561  diftpsn3  3563  difpr  3564  snsspr1  3570  snsspr2  3571  prss  3578  prssg  3579  2ordpr  4315  xpsspw  4520  dmpropg  4871  rnpropg  4878  funprg  5031  funtp  5034  fntpg  5037  f1oprg  5260  fnimapr  5329  fpr  5444  fprg  5445  fmptpr  5454  fvpr1  5464  fvpr1g  5466  fvpr2g  5467  df2o3  6151  unfiexmid  6582  prfidisj  6591  pr2nelem  6766  fzosplitprm1  9576  hashprg  10116  sumpr  10694  bdcpr  11231
  Copyright terms: Public domain W3C validator