Definition df-pr 3050

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For a more traditional definition, but requiring a dummy variable, see dfpr2 3059.

Assertion

Ref	Expression
df-pr	|- {A, B} = ({A} u. {B})

Detailed syntax breakdown of Definition df-pr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cpr 3045	. 2 class {A, B}
4	1	csn 3044	. . 3 class {A}
5	2	csn 3044	. . 3 class {B}
6	4, 5	cun 2591	. 2 class ({A} u. {B})
7	3, 6	wceq 1298	1 wff {A, B} = ({A} u. {B})

This definition is referenced by:  dfsn2 3057  dfpr2 3059  prcom 3097  preq1 3098  prprc1 3108  snsspr1 3135  prss 3138  prssg 3140  pwssun 3578  xpsspw 4093  dmprop 4369  funprg 4466  funtp 4468  fpr 4810  fprOLD 4811  df2o2 5186  prfi 5647  rankpr 5803  xp2cda 6078  renfdisjOLD 6713  ssxr 6714  spanpr 11136  superpos 11926  isprm2lem 13774  altopth2sn 14091  unpde2eg2 14406  repfuntw 14502  fnimapr 15687  smprngpr 16200

Copyright terms: Public domain