Definition df-pr 2417

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 2426.

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 2414	. 2 class {A, B}
4	1	csn 2413	. . 3 class {A}
5	2	csn 2413	. . 3 class {B}
6	4, 5	cun 2048	. 2 class ({A} u. {B})
7	3, 6	wceq 958	1 wff {A, B} = ({A} u. {B})

This definition is referenced by:  dfsn2 2424  dfpr2 2426  prcom 2451  preq1 2452  prprc1 2456  pwssun 2833  xpsspw 3263  df2o2 4147  prfi 4568  prfiOLD 4569  rankpr 4702  xp2cda 4940  renfdisj 5551  spanpr 9498  superpos 10276  unpde2eg2 10530

Copyright terms: Public domain