Definition df-pr 2471

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

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 2468	. 2 class {A, B}
4	1	csn 2467	. . 3 class {A}
5	2	csn 2467	. . 3 class {B}
6	4, 5	cun 2097	. 2 class ({A} u. {B})
7	3, 6	wceq 992	1 wff {A, B} = ({A} u. {B})

This definition is referenced by:  dfsn2 2478  dfpr2 2480  prcom 2508  preq1 2509  prprc1 2515  pwssun 2905  xpsspw 3346  df2o2 4277  prfi 4700  rankpr 4838  xp2cda 5080  renfdisj 5693  spanpr 9779  superpos 10562  unpde2eg2 10825

Copyright terms: Public domain