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

Definition df-pr 3538
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 3606. For a more traditional definition, but requiring a dummy variable, see dfpr2 3550. (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 3532 . 2  class  { A ,  B }
41csn 3531 . . 3  class  { A }
52csn 3531 . . 3  class  { B }
64, 5cun 3073 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1332 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3545  dfpr2  3550  ralprg  3581  rexprg  3582  disjpr2  3594  prcom  3606  preq1  3607  qdass  3627  qdassr  3628  tpidm12  3629  prprc1  3638  difprsn1  3666  diftpsn3  3668  difpr  3669  snsspr1  3675  snsspr2  3676  prss  3683  prssg  3684  iunxprg  3900  2ordpr  4446  xpsspw  4658  dmpropg  5018  rnpropg  5025  funprg  5180  funtp  5183  fntpg  5186  f1oprg  5418  fnimapr  5488  fpr  5609  fprg  5610  fmptpr  5619  fvpr1  5631  fvpr1g  5633  fvpr2g  5634  df2o3  6334  enpr2d  6718  unfiexmid  6813  prfidisj  6822  pr2nelem  7063  xp2dju  7087  fzosplitprm1  10041  hashprg  10585  sumpr  11213  strle2g  12087  bdcpr  13238
  Copyright terms: Public domain W3C validator