Definition df-pr 3695

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so { A , B } = { B , A } as proven by prcom 3766. For a more traditional definition, but requiring a dummy variable, see dfpr2 3707. (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 3689	. 2 class { A , B }
4	1	csn 3688	. . 3 class { A }
5	2	csn 3688	. . 3 class { B }
6	4, 5	cun 3208	. 2 class ( { A } u. { B } )
7	3, 6	wceq 1398	1 wff { A , B } = ( { A } u. { B } )

This definition is referenced by:  dfsn2  3702  dfpr2  3707  ralprg  3739  rexprg  3740  disjpr2  3752  prcom  3766  preq1  3767  qdass  3787  qdassr  3788  tpidm12  3789  prprc1  3799  difprsn1  3832  diftpsn3  3834  difpr  3835  snsspr1  3841  snsspr2  3842  prss  3849  prssg  3850  iunxprg  4071  2ordpr  4645  xpsspw  4861  dmpropg  5234  rnpropg  5241  funprg  5405  funtp  5408  fntpg  5411  f1oprg  5659  fnimapr  5736  fpr  5865  fprg  5866  fmptpr  5875  fvpr1  5887  fvpr1g  5889  fvpr2g  5890  df2o3  6661  enpr2d  7063  unfiexmid  7177  prfidisj  7186  tpfidceq  7189  pr2nelem  7487  xp2dju  7521  fzosplitpr  10575  fzosplitprm1  10576  hashprg  11168  sumpr  12092  strle2g  13309  perfectlem2  15855  bdcpr  16628