Definition df-pr 3743

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, A e. { 1 , -u 1 } -> (A ^ 2 ) = 1 (ex-pr in set.mm). They are unordered, so {A, B} = {B, A} as proven by prcom 3799. For a more traditional definition, but requiring a dummy variable, see dfpr2 3750. (Contributed by NM, 5-Aug-1993.)

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 3739	. 2 class {A, B}
4	1	csn 3738	. . 3 class {A}
5	2	csn 3738	. . 3 class {B}
6	4, 5	cun 3208	. 2 class ({A} u. {B})
7	3, 6	wceq 1642	1 wff {A, B} = ({A} u. {B})

This definition is referenced by:  dfsn2  3748  dfpr2  3750  ralprg  3776  rexprg  3777  prcom  3799  preq1  3800  qdass  3820  qdassr  3821  tpidm12  3822  difprsn1  3848  diftpsn3  3850  snsspr1  3857  snsspr2  3858  prss  3862  prssg  3863  ssunpr  3869  sstp  3871  prex  4113  snprss1  4121  prprc2  4123  dmpropg  5069  funprg  5150  funprgOLD  5151  fnimapr  5375  fpr  5438  fvpr1  5450  1p1e2c  6156  el2c  6192  ce2  6193