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

Definition df-pr 3424
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 3487. For a more traditional definition, but requiring a dummy variable, see dfpr2 3436. (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 3418 . 2  class  { A ,  B }
41csn 3417 . . 3  class  { A }
52csn 3417 . . 3  class  { B }
64, 5cun 2981 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1285 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3431  dfpr2  3436  ralprg  3462  rexprg  3463  disjpr2  3475  prcom  3487  preq1  3488  qdass  3508  qdassr  3509  tpidm12  3510  prprc1  3519  difprsn1  3545  diftpsn3  3547  difpr  3548  snsspr1  3554  snsspr2  3555  prss  3562  prssg  3563  2ordpr  4296  xpsspw  4499  dmpropg  4844  rnpropg  4851  funprg  5001  funtp  5004  fntpg  5007  f1oprg  5221  fnimapr  5287  fpr  5399  fprg  5400  fmptpr  5409  fvpr1  5419  fvpr1g  5421  fvpr2g  5422  df2o3  6100  unfiexmid  6464  prfidisj  6473  pr2nelem  6596  fzosplitprm1  9397  hashprg  9909  bdcpr  10954
  Copyright terms: Public domain W3C validator