Definition df-pr 1812

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

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 1809	. 2 class {A, B}
4	1	csn 1808	. . 3 class {A}
5	2	csn 1808	. . 3 class {B}
6	4, 5	cun 1485	. 2 class ({A} u. {B})
7	3, 6	wceq 1091	1 wff {A, B} = ({A} u. {B})

This definition is referenced by:  dfsn2 1819  dfpr2 1821  prprc 1839  prcom 1840  preq1 1870  pwssun 1917  xpex 2488  df2o2 3112  prfi 3444  rankpr 3536  xp2cda 3723

metamath.org