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

Definition df-pr 3409
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 3473. For a more traditional definition, but requiring a dummy variable, see dfpr2 3421. (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 3403 . 2  class  { A ,  B }
41csn 3402 . . 3  class  { A }
52csn 3402 . . 3  class  { B }
64, 5cun 2942 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1259 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3416  dfpr2  3421  ralprg  3448  rexprg  3449  disjpr2  3461  prcom  3473  preq1  3474  qdass  3494  qdassr  3495  tpidm12  3496  prprc1  3505  difprsn1  3530  diftpsn3  3532  snsspr1  3539  snsspr2  3540  prss  3547  prssg  3548  2ordpr  4276  xpsspw  4477  dmpropg  4820  rnpropg  4827  funprg  4976  funtp  4979  fntpg  4982  f1oprg  5195  fnimapr  5260  fpr  5372  fprg  5373  fmptpr  5382  fvpr1  5392  fvpr1g  5394  fvpr2g  5395  df2o3  6044  fzosplitprm1  9191  bdcpr  10357
  Copyright terms: Public domain W3C validator