Definition df-pr 3640

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 3709. For a more traditional definition, but requiring a dummy variable, see dfpr2 3652. (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 3634	. 2 class { A , B }
4	1	csn 3633	. . 3 class { A }
5	2	csn 3633	. . 3 class { B }
6	4, 5	cun 3164	. 2 class ( { A } u. { B } )
7	3, 6	wceq 1373	1 wff { A , B } = ( { A } u. { B } )

This definition is referenced by:  dfsn2  3647  dfpr2  3652  ralprg  3684  rexprg  3685  disjpr2  3697  prcom  3709  preq1  3710  qdass  3730  qdassr  3731  tpidm12  3732  prprc1  3741  difprsn1  3772  diftpsn3  3774  difpr  3775  snsspr1  3781  snsspr2  3782  prss  3789  prssg  3790  iunxprg  4008  2ordpr  4573  xpsspw  4788  dmpropg  5156  rnpropg  5163  funprg  5325  funtp  5328  fntpg  5331  f1oprg  5568  fnimapr  5641  fpr  5768  fprg  5769  fmptpr  5778  fvpr1  5790  fvpr1g  5792  fvpr2g  5793  df2o3  6518  enpr2d  6913  unfiexmid  7017  prfidisj  7026  tpfidceq  7029  pr2nelem  7301  xp2dju  7329  fzosplitprm1  10365  hashprg  10955  sumpr  11757  strle2g  12972  perfectlem2  15505  bdcpr  15844