Definition df-pr 2413

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

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 2410	. 2 class {A, B}
4	1	csn 2409	. . 3 class {A}
5	2	csn 2409	. . 3 class {B}
6	4, 5	cun 2045	. 2 class ({A} u. {B})
7	3, 6	wceq 956	1 wff {A, B} = ({A} u. {B})

This definition is referenced by:  dfsn2 2420  dfpr2 2422  prcom 2447  preq1 2448  prprc1 2452  pwssun 2827  xpsspw 3257  df2o2 4141  prfi 4555  prfiOLD 4556  rankpr 4692  xp2cda 4928  renfdisj 5539  spanpr 9503  superpos 10281  unpde2eg2 10544

Copyright terms: Public domain