Definition df-pr 2418

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

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

This definition is referenced by:  dfsn2 2425  dfpr2 2427  prcom 2452  preq1 2453  prprc1 2457  pwssun 2834  xpsspw 3264  df2o2 4148  prfi 4570  prfiOLD 4571  rankpr 4709  xp2cda 4947  renfdisj 5558  spanpr 9505  superpos 10284  unpde2eg2 10538

Copyright terms: Public domain