Definition df-pr 2409

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

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 2406	. 2 class {A, B}
4	1	csn 2405	. . 3 class {A}
5	2	csn 2405	. . 3 class {B}
6	4, 5	cun 2041	. 2 class ({A} u. {B})
7	3, 6	wceq 954	1 wff {A, B} = ({A} u. {B})

This definition is referenced by:  dfsn2 2416  dfpr2 2418  prcom 2443  preq1 2444  prprc1 2448  pwssun 2822  xpsspw 3252  df2o2 4131  prfi 4537  rankpr 4672  xp2cda 4908  renfdisj 5520  spanpr 9443  superpos 10218

Copyright terms: Public domain